Proof theory for theories of ordinals—I: recursively Mahlo ordinals Original Research Article

This paper deals with a proof theory for a theory T22 of recursively Mahlo ordinals in the form of Π2-reflecting on Π2-reflecting ordinals using a subsystem Od(μ) of the system O(μ) of ordinal diagrams in Arai (Arch. Math. Logic 39 (2000) 353). This paper is the first published one in which a proof-theoretic analysis à la Gentzen–Takeuti of recursively large ordinals is expounded.