How to characterize provably total functions by local predicativity
Andreas Weiermann · Journal of Symbolic Logic · 1996
Abstract Inspired by Pohlers' proof-theoretic analysis of KPω we give a straightforward non-metamathematical proof of the (well-known) classification of the provably total functions of PA, PA + TI(⊰ ↾) (where it is assumed that the well-ordering ⊰ has some reasonable closure properties) and KPω. Our method relies on a new approach to subrecursion due to Buchholz, Cichon and the author.