FORMALIZED RECURSIVE FUNGTICNALS AND FORMALIZED REALIZABILITY S. G. KLEENJi The University of Wisconsin CONTENTS Introduction 1 PART I. FORMALIZED RECURSIVE FUNGTICNALS § 1. Computation tree numbers 2 § 2. p-terms and p-functors rc^s (definition and basic properties) 22 § 3. Representation of p~terms by proper Indices 53 § 4. The recursion theorem the normal form theorem £T)LCQ and hoc uM JR & CA(R)] 67 PART II. FORMALIZED REALIZABILITY § 5o Intuitionistically provable formulas are realizable and (a)~realizable 77 References 104 Introduction. In Kleene and Vesley 1965 ("The Foundations of Intuitionistic Mathematics", hereafter cited as "FIM") pp. 110-111, we proposed a formal treatment of realizability. We anticipated that by formalization the model-theoretic consistency proof in FBI for the intuitionistic formal system of analysis can be made into a metamathematical consistency proof relative to the basic system (i.e. the common part of the intuitionistic and classical systems). Further, at the last two Congresses for Logic, Methodology and Philosophy of Science, we stated results whose full proofs require a formal treatment of realizability. Thus, in 1964a p. 42, e.g. we showed, contingently on such formalization, that any prenex formula provable in the intuitionistic system of analysis is provable in the basic system. In 1967a, e.g. we argued, contingently on the use of another formalized realizability notion, that, if a closed formula Vx3yA(x,y) is provable in the intuitionistic system of analysis, then so is Vx3y[T, (e,x,y) & A(x,U(y))] for some Received by the editors The research resulting in this Memoir was carried out over an extended period, during parts of which it was supported by Grants GP-1621, GP-4257, GP-5913 and GP-8569 of the National Science Foundation of the U.S.A. A summary was presented in a talk on August 19, 1963 at the Summer Conference in Intuitionism and Proof Theory at the State University of New York at Buffalo.
Previous Page Next Page