A slow growing analogue to Buchholz' proof (Q1182465)

To show that heroic Hercules always chops off all heads of heinous Hydrae, but, alas, that mathematical proofs of this fact are hard to achieve, \textit{W. Buchholz} used the term structure \((T,\cdot[\cdot])\) to represent Hydrae and fast growing functions to size up the strength of a mathematical theory [ibid. 33, 131-155 (1987; Zbl 0636.03052)]. Among other things, he characterized the provably total recursive functions in terms of fast growing functions. It is this characterization theorem whose analogue the author proves in terms of slow growing functions, \(G_ n\), \(n<\omega\). And, as he stated, the proof is ``a slight modification of Buchholz's''. The author summarizes the contents of this paper in two theorems. (I) \(\text{GID}_ \nu\vdash \forall n \exists m(a[n]^ m=0)\) for each \(a\in T_ 0(\nu)\). (II) If \(\text{GID}_ \nu \vdash \forall x \exists y \phi(x,y)\), where \(\phi\) is a \(\Sigma^ 0_ 1\)-formula, then (a) \(\exists n_ 0 \forall n\geq n_ 0 \exists m<G_ 1(D_ 0 D^ n_ \nu 0)\phi(n,m)\), (b) \(\exists n_ 0 \forall n>0 \exists m<G_ n(D_ 0 D_ \nu^{n_ 0} 0)\phi(n,m)\), and (c) \(\exists n_ 0 \forall n\geq n_ 0 \exists m<G_ n(D_ 0 D_{\nu+1} 0)\phi(n,m)\). Here, \(\text{GID}_ \nu\), \(\nu\leq\omega\), is the theory with iterated inductive definitions. The paper is reading for adults; there are hardly any tales or illustrations.