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