Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math.independent

Topic: Interdeducibility of properties of an abstract consequence relation.
Replies: 11   Last Post: Mar 8, 2013 8:40 PM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Graham Cooper

Posts: 4,237
Registered: 5/20/10
Re: Interdeducibility of properties of an abstract consequence relation.
Posted: Mar 7, 2013 4:26 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Mar 7, 9:21 am, Frederick Williams <freddywilli...@btinternet.com>
wrote:
> Graham Cooper wrote:
> > there are simple variable renaming schemes that do away with
> > substitutions.

>
> > INFERENCES = 0
>
> > For Each New Formula, increment and append INFERENCES to every
> > variable name.

>
> > e.g.
>
> > Predicate
> > vert( line ( pnt( X , Y ) , pnt( X , Z )))

>
> > Goal?
> > vert( line ( pnt( 1 , 1 ) , pnt( 1, 5 )))  ?

>
> > Match
> > vert( line ( pnt( X1 , Y1 ) , pnt( X1 , Z1 )))

>
> > X1 = 1
> > Y1 = 1
> > X1 = 1
> > Z1 = 5

>
> > SUCCESS!
>
> > > Sub(M,x,y,N) means that for every alpha in M there is a beta in N such
> > > that Sub(alpha,x,y,beta) and every formula in N can be obtain thus from
> > > one in M.

>
> > Set at a time variable renaming?
>
> > Again I don't see what the utility is.
>
> It enables me to state P9 below.
>

> > > P9 If Sub(M,x,y,N), Sub(alpha,x,y,beta) and M |= alpha, then N |= beta.



Again I don't see what P9 is for.

formula1 [X/Y] = formula2

is standard substitution syntax.

---------------

Making Sub(..) a predicate still doesn't formalise the Quantifier
syntax

Try writing

WFF( p ) as a predicate

ProofByInduction( p(n) ) as a predicate

ProofByContradiction( p ) as a predicate


---------------

In my Shorthand for |-

Axiom1 & Axiom2 & Axiom3 & .... Axiomn -> Theorem1


it's quite neat in that a false axiom gives you a false theory!


Herc
--
www.BLoCKPROLOG.com




Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.