This paper deals with a proof theory for a theory T3 of Π3-reflecting ordinals using the system O(Π 3) of ordinal diagrams in Arai (J. Symbolic Logic 65 (2000) 1375). This is a sequel to the previous one (Ann. Pure Appl. Logic 122 (2003) 1) in which a theory for recursively Mahlo ordinals is analyzed proof-theoretically. © 2004 Elsevier B.V. All rights reserved.
Berardi, S., & Valentini, S. (2004). Krivine’s intuitionistic proof of classical completeness (for countable languages). Annals of Pure and Applied Logic, 129(1–3), 93–106. https://doi.org/10.1016/j.apal.2004.01.002