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