Y1' ... ,Yn) ::) x = y]. Hence, by rule (xii), <Jt. Rules (i)-(xiii) are now sufficient to establish <k\", also for any other term or wffoforder n + 1in the vocabulary of K.
Now letX = Q(y1' ... ,Yk ) be a wffof order n + 1 such that in all the stated circumstances M F Q(a1' ... , ak)' This implies M <I<l Q(a1' ... , ak) and hence M <I<l tj(ab ... , ak) for a'll descriptions tj which are contained in Q(Y1' ... ,Yk), although Y1, ... ,Yk need not appear effectively in all of them. By what has been proved already, we may conclude that <ltj(Y1' ... ,Yk). Suppose in particular that tb ... , tr are the descriptions of order n + 1 which appear in X, tj(y1' ... ,Yk) = [(txj)~(Xj,Y1' ... ,
Yk)]. Since <ltj(Y1' ... ,Yk) has been derived, this must have been done by means of rule (xii), implying that 1-(3xj)~(xj,Y1' ... ,Yk) and I-('t/Xj) ('t/zj ) [~(Xj'Y1' ... ,Yk) /\ ~(Zj'Y1' ... ,Yk) ::) Xj = Zj]. Also, by (xiii), I-Qj(t j6'l' ... ,Yk),Y1, ... J'k)' and so
(10.1 ) We may write Q in more detail as Q(t1' , tm'Yb ... ,Yk), indicating the appearance of the descriptions (t1' , tm) in Q. Then Q' (Yl, ... , Yk) = (3x1) ... (3xm) [Q(Xb ... , Xm'Y1' ,Yk) /\ Q1(X1,Y1, ... ,Yk) /\ ... /\ Qm(Xm'Y1' ... ,Yk)] is a wff of order n, at most. Also M F Q' (a 1, ... , ak) for all the M and (a b ... , ak) which have to be taken into account and so, by the inductive assumption,
Using familiar procedures of the lower predicate calculus, we obtain from (10.1)
where, for the sake of brevity, we have not displayed 0'1" .. ,ym). Also, from the last axiom scheme of (xi),
KVxj) [<2j(*j,J>'i, • • • , y k) D Xj = t j(yu . . . ,j)k)].