16

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

axioms.

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)

(v) X(yHKy,/2(y)).

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,