A logic of recursion

AbstractMoschovakis (1984, in “Computation and Proof Theory” (Y. Richter et al., Eds.), Lect. Notes in Math. Vol. 1104, pp. 289–362, Springer-Verlag, Berlin) raised a question: to find a “logic of recursion,” related to “recursion structures” as denotational models of the language of recursion investigated in the same paper. We give a positive answer to this question. The “logic of recursion” presented in our paper is a first-order many-sorted β-logic (cf. Girard, (in press), “Proof Theory and Logical Complexity,” Vol. 2, Bibliopolis, Napoli), modified in order to deal with function symbols interpreted as partial functions, and extended with the operators λ (abstraction), R (recursion), I (iteration along the ordinal numbers). The operators λ and R are already present in Moschovakis' languages of recursion. The use of the operator I together with first-order many-sorted β-logic is needed for obtaining the completeness theorem