Let T(Ω) be the ordinal notation system from Buchholz-Schütte (1988). [The order type of the countable segmentT(Ω)0 is — by Rathjen (1988) — the proof-theoretic ordinal the proof-theoretic ordinal ofACA 0 + (Π 1 l −TR).] In particular let ↦Ω a denote the enumeration function of the infinite cardinals and leta ↦ ψ0 a denote the partial collapsing operation on T(Ω) which maps ordinals of T(Ω) into the countable segment TΩ 0 of T(Ω). Assume that the (fast growing) extended Grzegorczyk (...) hierarchy $(F_a )_{a \in T(\Omega )_0 }$ and the slow growing hierarchy $(G_a )_{a \in T(\Omega )_0 }$ are defined with respect to the natural system of distinguished fundamental sequences of Buchholz and Schütte (1988) in the following way: $$\begin{array}{*{20}c} {G_0 (n): = 0,} & {F_0 (n): = (n + 1)^2 ,} \\ {\begin{array}{*{20}c} {G_{a + 1} (n): = G_a (n) + 1,} \\ {G_l (n): = G_{l[n]} (n),} \\ \end{array} } & {\begin{array}{*{20}c} {F_{a + 1} (n): = \underbrace {F_a (...F_a }_{n + 1 - times}(n)...),} \\ {F_l (n): = F_{l[n]} (n),} \\ \end{array} } \\ \end{array}$$ wherel is a countable limit ordinal (term) and (l[n]) n ∈N is the distinguished fundamental sequence assigned tol. For each ordinal (term)a in T(Ω) and each natural numbern letC n (a) be the formal term which results from the ordinal terma by successively replacing every occurence ofψ a by $\psi _{ - 1 + C_n (a)}$ whereψ −1 is considered as a defined function symbol, namely $\psi _{ - 1} b: = F_{\psi _0 b + 1} (n + 1)$ . (Note thatψ a 0=Ω a ) In this article it is shown that for each ordinal termψ 0 a in T(Ω) there exists a natural numbern 0 such thatψ 0 C n (a) ∈ T(Ω) and $G_{\psi _0 a} (n) \leqslant F_{\psi _0 C_n (a) + 1} (n + 1)$ holds for alln≥n 0. This hierarchy comparison theorem yields a plethora of new results on nontrivial lower bounds for the slow growing ordinals — i.e. ordinals for which the slow growing hierarchy yields a classification of the provably total functions of the theory in question — of various theories of iterated inductive definitions (and subsystems ofKPi) and on the number and size of the subrecursively inaccessible ordinals — i.e. ordinals at which the extended Grzegorczyk hierarchy and the slow growing hierarchy catch up — below the proof-theoretic ordinal ofACA 0+(Π 1 l −TR). In particular these subrecursively inaccessibles ordinals are necessarily of the form $\psi _0 \Omega ..._{\Omega _\omega }$. (shrink)

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(\prec\lceil)$ (where it is assumed that the well-ordering $\prec$ has some reasonable closure properties) and KPω. Our method relies on a new approach to subrecursion due to Buchholz, Cichon and the author.

Herbrand's Theorem, in the form of $$\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{\exists } $$ -inversion lemmata for finitary and infinitary sequent calculi, is the crucial tool for the determination of the provably total function(al)s of a variety of theories. The theories are (second order extensions of) fragments of classical arithmetic; the classes of provably total functions include the elements of the Polynomial Hierarchy, the Grzegorczyk Hierarchy, and the extended Grzegorczyk Hierarchy $\mathfrak{E}^\alpha $ , α < ε0. A subsidiary aim of the paper is to show (...) that the proof theoretic methods used here are distinguished by technical elegance, conceptual clarity, and wide-ranging applicability. (shrink)

It is well known that the Ackermann function can be defined via diagonalization from an iteration hierarchy which is built on a start function like the successor function. In this paper we study for a given start function g iteration hierarchies with a sub-linear modulus h of iteration. In terms of g and h we classify the phase transition for the resulting diagonal function from being primitive recursive to being Ackermannian.