Abstract.
Let T be Gödel's system of primitive recursive functionals of finite type in a combinatory logic formulation. Let \(T^{\star}\) be the subsystem of T in which the iterator and recursor constants are permitted only when immediately applied to type 0 arguments. By a Howard-Schütte-style argument the \(T^{\star}\)-derivation lengths are classified in terms of an iterated exponential function. As a consequence a constructive strong normalization proof for \(T^{\star}\) is obtained. Another consequence is that every \(T^{\star}\)-representable number-theoretic function is elementary recursive. Furthermore, it is shown that, conversely, every elementary recursive function is representable in \(T^{\star}\).
The expressive weakness of \(T^{\star}\) compared to the full system T can be explained as follows: In contrast to \(T\), computation steps in \(T^{\star}\) never increase the nesting-depth of \({\mathcal I}_\rho\) and \({\mathcal R}_\rho\) at recursion positions.
Similar content being viewed by others
Author information
Authors and Affiliations
Additional information
Received: 3 July 1996/ Revised version: 24 September 1999
Rights and permissions
About this article
Cite this article
Beckmann, A., Weiermann, A. Characterizing the elementary recursive functions by a fragment of Gödel's T. Arch Math Logic 39, 475–491 (2000). https://doi.org/10.1007/s001530050160
Issue Date:
DOI: https://doi.org/10.1007/s001530050160