On Mar 9, 5:46 am, Frederick Williams <freddywilli...@btinternet.com> wrote: > Graham Cooper wrote: > > > > > On Mar 7, 9:21 am, Frederick Williams <freddywilli...@btinternet.com> > > > > wrote: > > > > > > 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. > > My (or rather, Hermes's) notation Sub(alpha,x,y,beta) signifies that > alpha, x, y and beta stand in a certain relation to one another. > Furthermore that relation is carefully defined. (If it isn't carefully > defined _in my post_, then the fault is mine and I shall rectify it.) > What does the "standard" definition mean? Standard may be good, > understandable is better. >
You've never seen
f(X+1) [Y/X] = f(Y+1) ?
Making SUBS a predicate has no purpose and neither does formalising variable renaming in Quantified logic.
As opposed to Lambda Calculus where substituting [Y/X] is used in the computation.