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

x_

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.