
Re: Interdeducibility of properties of an abstract consequence relation.
Posted:
Mar 7, 2013 4:26 PM


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

