4 S. C. KLEENE
(cf. FIM p. 12 Lemma 3.2 the square-bracketed version, and for an application
p. 106 line 3 from below). Hence we now generalize from sequence numbers to
allow for inputs not necessarily consisting of consecutive values; e.g. if the
input of information about oc consists of the values o((0), gc(3)and oC(k)9
we shall represent it by ^(0)*fl.£|(3)+1-pJ(4)+1. Let b|* =
(iJ'OnjCk)*^0"^^)*83 2t(i)+1! so ^ ^ "kl^"says that b represents a finite
selection of values of gc in this manner.
Our main objective is a formalized theory. So now we let nb|*n be an
abbreviation for a standard (prime) formula (FIM pp. 27 ff.) such that *2&.la
holds (and hence expressing b|o^)a Also (later) we shall use
nb15##.,bfl \o(-^9.••,&.£ to abbreviate b1 Io^ & ... & b- | tfn for any i 0,
and similarly informally (with italic instead of Roman letters).
Throughout this Part I, "h" can be read as expressing provability (or
deducibility) in the basic system, or actually in the system obtained thence
by omitting the bar theorem Ax. Sch. 26,3 (FIM p. 54) and weakening Ax. Sen.
X2.1 (FIM p. 14)to:7
X2.2J. Vx3iyA(x,y) z 3xVxA(x,*(x)).
The numbering below continues from that in Chapter I of FIM.
We can regard "B-. & ... & B0" for i = 0 as standing for some closed
provable formula, say 0=0; so A & b..,...,b0 I 06,..., oC 0 simplifies then to A.
The list f..,...,f of function symbols and Postulate Group D of the basic
system (FIM p. 19)will be extended here a bit beyond § 5 of FIM (at 3O.I,
x31.1, x31.2; cf. end1.5).
'This is the system called (1,0,0)by Joan Rand Moschovakis in 1965* 1967•
In this Part I, our proofs are presented as in the basic system. Butx26.3 is
not used. There is just one "primary" use ofx2.1, namely via --2.2 in the
proof of -»32.3 (besides which --32.3 is thereafter used); and for this use (and
the one for (11) in Part II 5.9), by Lemma 8 x2.2! would suffice instead.
The use ofx2.2I (orx2.2 orx2.1) for #32.3 and results depending on it is
unavoidable; i.e. we can't get by here with Moschovakis' "least system"
(0,0,0). For, Moschovakis 1965 2.4 shows that VxzUyA(x,y) is provable in
(0,0,0) for a certain formula A(x,y) numeralwise representing AckermannTs
nonprimitive recursive function f(x) (IM p. 272).So if (0,0,0) sufficed here
and hence for the J^_ in 5.10 (Part II), then by (iv) in 5.93otVxA(x, c*(x))
would be provable in (0,0,0), contrary to the interpretation of (0,0,0) given
by Moschovakis in 1965, 1967 with the primitive recursive functions as the
range of the function variables.
The formulas we now establish through --34.26 would fit best at the end of
FIM § 5 (p. 43). But we skip to numbers --28.— etc., since --26.— and -"27.—
are used in FIM §§ 6, 7.