FORMALIZED RECURSIVE FUNCTIONALS
(vii) y=(y)0,(y)x = (y)^, y=(y)0, (j\9 (y)2 = (y^y & (y)2y.
Now consider how "Cpu occurs in D(y)# Each occurrence is in one of the
"y=(y)0,(y)1 & cpKy^)", "y^(y)0,(y)1,(y)2 & °p((y)i)& GP((y)2)n-
Let us write D(y) as "DCy=(y)0,(y)1 & Cp((y).,),...] where, here and in each
variant below, ".••" stands for a formula like the one just preceding it but
with y=(y)0,(y)1,(y)2 etc. Then D(y,z) is D[y=(y)0,(y)^ & (z)(y) =0,...].
Now Cp(y) ~ (ccp(yf)) =0 [def. of Cpl
~ D(y,ccp(y)) [by r(y,z)=0~ D(y,z)]
— DCy=(y)0,(y)1 & (ccp(y))(y) =0,...] [def. of Df JJ
~ DCy=(y)0,(y)1 & (y)-^ & (ccp(y))^ =0,...] [(vii), prop, calcj
— Dry=(y)0, (y)^ & (y^y & (ccpUy)^))
^ =0,...] [(vi»), logic]
-Di:y=(y)0,(y)1 & (y) ^ & CpUy)^,...] [def. of Cp]
— D[y=(y)0,(y)1 & CpCCy^),...] [(vii), prop, calcj
~ D(y) [def. of D[ 11.
Thus I - Cp(y) — D(y), which is *31.3. -
On the basis of *31*3 we shall develop the theory of partial recursive
functions of type 0 and 1 variables, in the basic system of FIM as construed
now to include the function symbolsand axioms up through ccp and 31»1, 31«2»
Of course,by eliminability theory (IM p. 415 Example 9, slightly
adapted to fit in FIM), we could find instead a composite formula Cp(y) so
that *31*3 holds in the basic system as it stood in FIM (or in even less).
Also, back at *30.1 we could have simply construed "aob" as an abbreviation
for the right member. But there can be no objection intuitionistically to
the new axioms ^30.1, ^1.1 and j}1.2 any more than to those in Group D up
to the point reached in FIM § 5» It would be contrary to the spirit of FIM to
go to extra work now just in order to stop with those only (cf. FIM p. 19
§ 5 TI2).
1.6. We begin the formal development now by establishing some funda-
mental properties of computation tree numbers. For *31.5b, k and i are any
numbers 0; and likewise in similar situations below when nototherwise stated.