S. C. KLEENE
formalized) will be provable (as *31.3 will state).
For brevity, we write lfD(y)" for the disjunction Cp^^y) V ••• V Cpg(y)
(with Cp(y) still an unspecified formula). Let D(y,z) result from D(y)by
replacing each part of D(y) of the form Cp(s) with s a term (actually s is
either (y).. or (y)o)ky (z)=0 (z a new number variable). So, while we don't
have D(y) as a known formula yet, we do know D(y,z). Indeed, by FIM pp. 27 ff.
we can build up a term r(y,z) in the basic system as given up through FIM i 5
such that h r(y,z)L and h r(y,z)=0 ~D(y,z).
Now we introduce a new function symbol ccp (as t^/)9 with ccp(y)
interpreted as expressing the course-of-values function cp(jr)for the
representing function cp(y) of Cp(y)j and we postulate the following two new
x31.1. ccp(0)=l. X31.2. ccp(y')^cp(y).p^7'ccp(3r)).
These fit the form (b) of FIM p. 20.Finally, we take Cp(y) to be (ccp(y!)) =0.
Now we are ready to establish that Cp(y) is a standard formula such that
h Cp(y) ~ D(y), as expressed by the following two results.
*31.3. I - Cp(y) ~ Cp0a(y) V ... V Cp8(y). *31.4. I (ccp(y'))yL.
PROOFS. Consider p. 40 of FIM "(c)WITH 'oi(y)"* We use this passage,
reinterpreting "g" as an abbreviation for ccp (rather than a function
variable) and "ot« as an abbreviation for Xy (B(yf)) • Then (i) p. 40 is
provable by 31.1 and 31.2 (with V- an^ &-introd.), and (ii)by 0.1 simply.
So the discussion there establishes the provability of (iii), (iv) and (using
(iv) in the ot(y)=~r(y,ac(y))at the end)
Translating (v) back into our symbolism (and using 0.1),
(vf) (ccp(yO) =r(y,ccp(y)).
Now #31.4 follows by substitution into r(y,z)L. Continuing by (iv) and -»24.2,
(vi) z$ r ( e(y))z=(3t(y))z=x(Z).
Translating into our symbolism (and using 0.1),
(vi«) zy o (ccp(y))z=(ccp(z'))z*
By *19.2 with *18.5, *3.9 and *129,