FORMALIZED RECURSIVE FUNCTIONALS

17

(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

two contexts

"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

~r(y,ccp(y))=0 [(v»)]

~ 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.