A logic of recursion (Q1262303)

A language for partial function(al)s on arbitrary structures dealing with application, abstraction, recursion and iteration along the ordinal numbers is considered, and a completeness theorem is established for some axiomatization in terms of modified Girard's \(\beta\)-logic. It is suggested to consider this as the axiomatization of a ``logic of recursion'' in the sense of \textit{Y. Moschovakis} [Lect. Notes Math. 1104, 289-364 (1984; Zbl 0599.03052)].