Ordinal diagrams for recursively Mahlo universes (Q1576592)

The paper under review is part of a great project of the author which continues the work of G. Gentzen and G. Takeuti, aiming at establishing the proof-theoretic strength of subsystems \(T_N\) of analysis. These systems are characterized by differently strong axiom schemata of \(\Pi_N\)-reflection (\(N\geq 2\)). The strength of a system \(T\) can be described by its proof-theoretic ordinal \[ |T|_{\Pi^{\Omega}_2}:=\inf\{\alpha\leq \omega^{CK}_1\mid\forall \Pi_2\text{-sentences }A(T\vdash A^{\Omega}\Rightarrow A^{\alpha})\}. \] In the considered paper \(N\) is to be 2. Let \(\mu\) be the least recursively Mahlo ordinal. \(\varkappa\) is called recursively Mahlo iff \(\varkappa\) is \(\Pi_2\)-reflecting on admissibles (i.e. on recursively regular ordinals). \(\varkappa\) is called \(\Pi_2\)-reflecting on admissibles if every \(\Pi_2\)-formula with parameters from \(\mathcal{L}_{\varkappa}\), the \(\varkappa\)-th element of the constructible hierarchy which is valid in \(\mathcal{L}_{\varkappa}\) is already valid in \(\mathcal{L}_{\varrho}\) for some admissible \(\varrho< \varkappa\). The author establishes an ordinal system \(O(\mu)\) of so-called ordinal diagrams starting with the symbols \(0\), \(\Omega\), \(\mu\),\(+\), \(\varphi\) and \(d\). \(\Omega\) is to represent the least admissible ordinal, + the usual addition, \(\varphi\) the Veblen functions and \(d\) something like the collapsing functions \(\psi\) introduced by \textit{W. Buchholz} in Ann. Pure Appl. Log. 32, 195-207 (1986; Zbl 0655.03038)]. Collapsing is permitted only with respect to \(\mu\) -- this yields admissible \(d_{\mu}\alpha\), and with respect to these \(\sigma= d_{\mu}\alpha\) -- this gives strongly critical not admissible ordinals \(d_{\sigma}\beta\). Together with \(O(\mu)\) simultaneously a binary relation \(<\) on \(O(\mu)\) is defined. The author proves: 1. The simultaneous definitions of \(O(\mu)\), \(<\), and certain auxiliary concepts, for instance sets of coefficients, are elementary recursive and can be formalized in the system \(S^1_2\) of bounded arithmetic of~~S. Buss. 2. \(<\) is a linear ordering of \(O(\mu)\). 3. \(<\) well-orders \(O(\mu)\). In the original version of the paper the author showed 1. and 2. simultaneously by a very long proof. Following a proposal of the referee, he separated both proofs by a slight modification of the definition. 3. is proved in the system \textbf{KPM} of set theory for recursively Mahlo universes by means of so-called distinguished classes, generalizing a method of \textit{W. Buchholz} [cf. ISILC Proof Theory Symp., dedic. Kurt Schütte, Proc. Int. Summer Inst., Logic Colloq., Kiel 1974, Lect. Notes Math. 500, 4-25 (1975; Zbl 0342.02021)]. Though obviously the system \(O(\mu)\) is closely related to set theory, the author reveals that he has no set-theoretic interpretation of \(O(\mu)\) at hand. The system is rather constructed in such a way that the proof of the Main Lemma in the submitted paper on ``Proof theory for theories of ordinals. I. Recursively Mahlo'' of the author can be executed. In a by now unpublished paper, the author of the paper under review presents a well-ordering proof for \(O(\mu)\) (and other systems) by means of inductive definitions.