18 S. C. KLEENE
*31.5a. * - Vy Vf VaVbYwVwfcp(y) & (y)0=f ,a,b,w &
Cp(y) & (y)0=f ,a,b,w 3 y=^ & w=w}.
*31.5b. f - Gp(y) & (y)
0
=f,^a
1
,..
#
,a
k
,i,b
1
,.
#
.,b
i
,w &
Cp(y) & (y)
0
=f,^a
1
,...,a
k
,^b
1
,...
f
b
i
,w3y= y & w=£.
(The part w=wineach follows by-*25.1from y=ywith (y)Q^...,w,(y)==...,w.)
PROOFS. *31.5a. Weusecourse-of-values induction ony (IMp. 193*l62b).
Assume thehyp. ind., sayvz(zy 3A(z)). Wemust deduce --31.5a as itstands,
i.e. A(y). Assume theantecedent oftheimplication inA(y).By Cp(y) with *3L3,
we have eleven cases Cp^Cy),...,Cpg(y). Twowill suffice forillustration.
CASE Ob: Cp0b(y). Byy=(y)0,(y)1,(y)2 inCP()b(y)with (vii) in the
proof of*31.3-*31.4, (y)^& (j)2y* - Now0= (y)Q^0
Q
Cby
(y)0=«0,(y)0^0 ±,... inCP()b(y)with *25.1 twice] = (f)Q [by (y)Q=f,a,b,w
similarly] = (y)Q
Q
[by (y)0=f,a,b,w]. But,using *31.3, in every casefor
Cp(y) except Cp0a(y) andCpob(y), (y)QQ ^0; so Cp0a(y) V CpQb(y). - Now
Cp0b(y) with (y)Q=f,a,b,w yields (y)Q
Q
^(f )
±
, (y)Qx=a, (y)Q2=b and
Gp((y)1) &
(J^O^WV^IW^O^.
Similarly either Cp~ (y) orCp^Cy) with (y)=f,a,b,w yields
So, since (y)^, thehyp. ind. ony applies to (y)1 with (y)-^,(f)1,a,b,
(y)-L o y(j\ o 3 as the ^f a^b*w^ and Sives (y)1=(y)1 & (y)1Q 3=(y)1
0
y
or more explicitly: First,we eliminate Vz from Vz(zy 3 A(z))using(y),
for z,i.e. as theterm t IMp. 99•Second, weusetheresult with (j)-^r and
3-elim. togetA((y)1). Third, we eliminate VyVfVaVbVwVw fromA^y^)
employing therespective terms listed above. Fourth, weusetheresult with
the conjunction ofthetwolast-displayed formulas via D-elim# to get
j)jr®l
&
^ l ^ ' ^ O ^ ~
B
^ ^ O ^
by GP0b(y)' ^ile Gp0a(^
_
would give (y)1
Q
j=0. Hence Cp^Cy). - NowGpQb(y), (y)Q=f,a,b,w, CpQb(y),
(y)0=f,a,b,w yield
Cp((y)2) & (y)2^0=f,3a,b,w & Cp((y)2) & (y)2^0=f,3a,b,w.
So thehyp. ind. applies again, to (y)2now, with (y)2,f,3a,b,w,w as the y,f,
a,b,w,w, andgives (y)2=s(y)2 & ***'• Hence also (y)Q=f,a,b,wf,a,b,w=y)0.
Previous Page Next Page