Proof theory for theories of ordinals. I: Recursively Mahlo ordinals (Q1400597)

In this paper, the author presents a proof-theoretic analysis of a theory of ``recursively Mahlo ordinals in the form of \(\Pi_2\)-reflecting on \(\Pi_2\)-reflecting ordinals''. As notation system, a subsystem of a system of ordinal diagrams, previously introduced by the same author [Arch. Math. Logic 39, 353-391 (2000; Zbl 0977.03030)], is used. There is no direct set-theoretic interpretation of the notation system, but it was extracted out of the cut-elimination proofs with some additional conditions to ensure foundation. In contrast to the proof-theoretic analysis of KPM by \textit{M. Rathjen} [Arch. Math. Logic 30, 377-403 (1991; Zbl 0727.03036)], which is carried out in the ``Schütte style'', the analysis here follows the ``Gentzen-Takeuti style'' [for the relation of the two approaches, cf., e.g., \textit{W. Buchholz}, Arch. Math. Logic 40, 255-272 (2001; Zbl 1007.03051)]. For an extension of the approach to \(\Pi_3\) reflection, one can consult recent work of \textit{M. Michelbrink} [Zur endlichen Behandlung der Beweistheorie schwacher Fragmente der Mengenlehre: KP + \(\Pi_3\)-Reflexion, PhD thesis, Universität Hannover, Fachbereich Mathematik und Informatik (2001), \url{http://www.cs.swan.ac.uk/~csmichel/Articles/Dissertation.pdf}].