Advances in Proof Theory pp 409-425 | Cite as

# Pointwise Transfinite Induction and a Miniaturized Predicativity

- 1 Citations
- 746 Downloads

## Abstract

The basis of this work is Leivant’s [6] theory of ramified induction over N, which has elementary recursive strength. It has been redeveloped and extended in various ways by many people; for example, Spoors and Wainer [13] built a hierarchy of ramified theories whose strengths correspond to the levels of the Grzegorczyk hierarchy. Here, a further extension of this hierarchy is developed, in terms of a predicatively generated infinitary calculus with stratifications of numerical inputs up to and including level \(\omega \). The autonomous ordinals are those below \(\Gamma _0\), but they are generated according to a weak (though quite natural) notion of transfinite induction whose computational strength is “slow” rather than “fast” growing. It turns out that the provably computable functions are now those elementary recursive in the Ackermann function (i.e. Grzegorczyk’s \(\omega \)th level). All this is closely analogous to recent works of Jäger and Probst [5] and Ranzi and Strahm [9] on iterated stratified inductive definitions, but their theories have full, complete induction as basis, whereas ours have only a weak, ramified form of numerical induction at bottom.

## Keywords

Computable Function Infinitary System Computation Rule Peano Arithmetic Fundamental Sequence## References

- 1.S. Bellantoni, S. Cook, A new recursion theoretic characterization of the polytime functions. Comput. Complex.
**2**, 97–110 (1992)MathSciNetCrossRefzbMATHGoogle Scholar - 2.W. Buchholz, An independence result for \(\Pi ^1_1\)-CA\(+\)BI. Ann. Pure Appl. Logic
**33**, 131–155 (1987)MathSciNetCrossRefzbMATHGoogle Scholar - 3.A. Cantini, Polytime, combinatory logic and positive safe induction. Arch. Math. Logic
**41**, 169–189 (2002)MathSciNetCrossRefzbMATHGoogle Scholar - 4.S. Feferman, Systems of predicative analysis II: representations of ordinals. J. Symbolic Logic
**33**(2), 193–220 (1968)MathSciNetCrossRefzbMATHGoogle Scholar - 5.G. Jäger, D. Probst, A proof theoretic analysis of theories for stratified inductive definitions in
*Gentzen’s Centenary: The Quest for Consistency*, ed. by R. Kahle, M. Rathjen (Springer, Cham, 2015), pp. 425–454Google Scholar - 6.D. Leivant, Intrinsic theories and computational complexity, in
*Logic and Computational Complexity*, ed. by D. Leivant, Springer Lecture Notes in Computer Science 960, pp. 177–194 Springer (1995)Google Scholar - 7.G. Mints, Finite investigations of transfinite derivations. J. Sov. Math.
**10**, 548–596 (1978). Translated from Zapiski Nauchnykh Seminarov. Steklova Akademii Nauk SSSR (LOMI), vol. 49, pp. 67–122 (1975)Google Scholar - 8.G.E. Ostrin, S.S. Wainer, Elementary arithmetic. Ann. Pure Appl. Logic
**133**, 275–292 (2005)MathSciNetCrossRefzbMATHGoogle Scholar - 9.F. Ranzi, T. Strahm, A note on the theory SID\(_{\le \omega }\) of stratified induction. Math. Logic Quart.
**60**(6), 487–497 (2014)Google Scholar - 10.U. Schmerl, Number theory and the Bachmann-Howard ordinal, in
*Logic Colloquium ’81*, ed. by J. Stern, North-Holland, pp. 287–298 (1982)Google Scholar - 11.H. Schwichtenberg, S.S. Wainer,
*Proofs and Computations*, ASL Perspectives in Logic (Cambridge University Press, Cambridge, 2012)zbMATHGoogle Scholar - 12.H. Simmons, The realm of primitive recursion. Arch. Math. Logic
**27**, 177–188 (1988)MathSciNetCrossRefzbMATHGoogle Scholar - 13.E.J. Spoors, S.S. Wainer, A hierarchy of ramified theories below PRA, in
*Logic, Construction, Computation*, ed. by U. Berger, H. Diener, P. Schuster, M. Seisenberger, Ontos Mathemaical Logic, vol. 3 (Ontos Verlag, 2012) pp. 475-499Google Scholar - 14.A. Weiermann, What makes a (pointwise) subrecursive hierarchy slow growing?, in
*Sets and Proofs*, Logic Colloquium ’97, ed. by S.B. Cooper, J.K. Truss, LMS Lecture Notes, vol. 258 (Cambridge University Press, 1999), pp. 403–423Google Scholar - 15.M. Wirz, Wellordering two sorts: a slow-growing proof theory for variable separation, Ph.D. thesis, Universität Bern (2005)Google Scholar