2 S. C. KLEENE

number £, where T- . and U express the predicate T, and function U of a

suitable version of our normal form theorem, p. 2&& of Kleene 1952b

("Introduction to Metamathematics", hereafter cited as "IM").

These projects for formalizing realizability theory must begin with a

formalization of the theory of general and partial recursive functions,or

"functionals", of number (type 0) and one-place number-theoretic function

(type 1) variables. Part I of the present paper gives such a formalization in

6 7

the basic formal system or less. l This not only supplies the underpinning

for such previously conjectured results,but also should provide basic

machinery for investigations of similar sorts.

Historical perspective, and an indication of how (after a number of

trials since the fall of 1959) we chose the method we are using for

formulating the theory of general and partial recursive functionals

preparatory to formalization, are given in our paper at the 1967 Tihany

Colloquium honoring Rdzsa Peter (Kleene 1968).

We shall repeat a little material from 1964a, 1967a and 1968, so that

the treatment here can be read presupposing only Chapters I-XII of IM,

$% 1-9 of FIM, and (only for the equivalence of the theory of recursive

functionals formalized here to other versions in the literature) a few

passages of Kleene 1959 that will be cited where they are used.

PART I. FORMALIZED RECURSIVE FUNCTIONALS

£ 1. Computation tree numbers. 1.1. We shall take it as known informally

that the partial recursive functions of our two types of variables can be

generated by repeated use of the following eight schemata. Here

TU*--" stand for lists of variables of the two types (»-#•» possibly empty).

For the moment, we use the convention that the order of variables of one type

relative to the other is immaterial, as in 1959 p. 3. (In our analysis

beginning in 1.2 below, we shall put the number variables first and the

function variables second, so a function with its independent variables will

(S1)-(S8) are the S1-S7 of Kleene 1959 p. 3, restricted to types 0 and 1,

and with S6 split into (S6) and (S8). (SO) takes the place of 310 p. 45.

3

Thereby we can write the schemata more compactly now. Beginning in 2.2,

a notational practice will be introduced that requires this convention to be

set aside.