Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory (Q2747729)

This paper is a further contribution to the program of metapredicativity [\textit{T. Strahm}, Lond. Math. Soc. Lect. Note Ser. 258, 383-402 (1999; Zbl 0961.03057); \textit{G. Jäger, R. Kahle, A. Setzer} and \textit{T. Strahm}, J. Symb. Log. 64, 53-67 (1999; Zbl 0937.03065)]. It was conjectured by P. Hancock, and proved by \textit{S. Feferman} [Stud. Logic Found. Math. 109, 171-196 (1982; Zbl 0522.03045)] that a natural constructive formulation of a chain of \(\omega\) inaccessible cardinals, represented as universes in type theory, has as proof-theoretical strength the Feferman-Schütte ordinal \(\Gamma_0\), which represents traditionally the ``upper limit'' of predicative systems. (This work is actually one of the motivations for the introduction of universes in explicit mathematics.) What is quite interesting is that there are natural further extensions of the notion of universes that cannot clearly be considered to be impredicative but whose proof-theoretical ordinals are strictly between \(\Gamma_0\) and the Bachmann-Howard ordinal. An example in the framework of type theory can be found in a recent paper [\textit{M. Rathjen}, Arch. Math. Log. 40, 207-233 (2001; Zbl 0990.03048)]. The term ``metapredicative'' refers to the fact that the analysis of such systems can be done without impredicative means but requires ordinal strength exceeding \(\Gamma_0\). NEWLINENEWLINENEWLINEThis paper presents a possible formulation of Mahlo universe in explicit mathematics and a detailed proof-theoretic analysis, with an exact computation of the ordinal strength. It presents also a formulation as an extension of Kripke-Platek set theory without \(\varepsilon\)-induction. One could probably as well formulate a metapredicative version of the type theory considered by \textit{A. Setzer} [Arch. Math. Log. 39, 155-181 (2000; Zbl 0943.03046)] by taking away \(W\)-types. The use of explicit mathematics, with partial operations, seems however really convenient to analyse the complex form of reflection introduced by the Mahlo axiom.