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
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.
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