A uniform approach for characterizing the provably total number-theoretic functions of KPM and (some of) its subsystems (Q1300010)

KPM in the title stands for Kripke-Platek-Mahlo, and the subsystems that the authors consider are KPi and KPl. (`i' is for `inaccessible', and `l' for `limit'.) The approach used is the one devised by the second author: use collapsing relations involving complexities of ordinal notations, and avoid meta-mathematical considerations. He gave a dry run of this approach on PA and \(\text{KP}\omega\) in a previous article [J. Symb. Log. 61, No. 1, 52-69 (1996; Zbl 0859.03028)], which is addressed to a ``wider readership'' than experts and is very elucidating. The synopsis of the paper under review is standard: first, ordinal notation systems, and theories, \(T\), like KPM are presented. Then a semi-formal system RS (ramified set theory), into which \(T\) is embedded. A careful analysis of cut elimination in RS gives, of a given provable \(\Pi_2\)-sentence \(\forall x \exists y\) \(A(x,y)\), an estimate of \(y\) from the given \(x\). As a conclusion, the authors give an exact characterization of the provably total functions of \(T\) in terms of all the Hardy functions \(H_\alpha\), \(\alpha< \|T\|\), the proof-theoretic ordinal of \(T\). An interesting result in the process is the \(\omega\)-boundedness: if \(T\) proves that the above sentence holds in \(L_\omega\), then indeed for an \(x\in L_\omega\), \(y\) can be found in \(L_n\), where \(n< \omega\) is found from \(x\) and some \(\alpha< \|T\|\).