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 T U*--" 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.
Previous Page Next Page