A logic of recursion

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

Authors

• V.Michele Abrusci
• Gianfranco Mascari

Keywords

No keywords are indexed for this paper.