Pointwise Transfinite Induction and a Miniaturized Predicativity

Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 28)


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.


Computable Function Infinitary System Computation Rule Peano Arithmetic Fundamental Sequence 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    S. Bellantoni, S. Cook, A new recursion theoretic characterization of the polytime functions. Comput. Complex. 2, 97–110 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    W. Buchholz, An independence result for \(\Pi ^1_1\)-CA\(+\)BI. Ann. Pure Appl. Logic 33, 131–155 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    A. Cantini, Polytime, combinatory logic and positive safe induction. Arch. Math. Logic 41, 169–189 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    S. Feferman, Systems of predicative analysis II: representations of ordinals. J. Symbolic Logic 33(2), 193–220 (1968)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 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. 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. 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. 8.
    G.E. Ostrin, S.S. Wainer, Elementary arithmetic. Ann. Pure Appl. Logic 133, 275–292 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 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. 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. 11.
    H. Schwichtenberg, S.S. Wainer, Proofs and Computations, ASL Perspectives in Logic (Cambridge University Press, Cambridge, 2012)zbMATHGoogle Scholar
  12. 12.
    H. Simmons, The realm of primitive recursion. Arch. Math. Logic 27, 177–188 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 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. 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. 15.
    M. Wirz, Wellordering two sorts: a slow-growing proof theory for variable separation, Ph.D. thesis, Universität Bern (2005)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.University of LeedsLeedsUK

Personalised recommendations