No label defined (Q4934569)

This paper determines the proof-theoretic strength of a particular system EMU of explicit mathematics which is based on a principle for the uniform construction of universes and the schema of formula induction. Systems of explicit mathematics were introduced by Solomon Feferman in the mid 70's, originally as a framework to formalize constructive mathematics in the sense of Bishop. Subsequently, systems of explicit mathematics (in particular those based on classical logic like EMU) turned out to be of importance in the context of the proof-theoretic analysis of subsystems of second-order arithmetic and set theory. Universes (which play an important role in type theories in the sense of Martin-Löf) were introduced into the context of explicit mathematics by Feferman in 1982 in connection with his proof of the so-called Hancock conjecture. The paper under review proves that EMU and the transfinitely iterated fixed point theory \(\widehat{\text{ID}}_{\leq \varepsilon_0}\) are proof-theoretically equivalent. The proof-theoretic ordinal of the latter (and hence also of EMU) is \(\varphi 1\varepsilon_00\) (for the ternary Veblen function \(\varphi)\) as was shown by \textit{G. Jäger}, \textit{R. Kahle}, \textit{A. Setzer} and \textit{T. Strahm} [J. Symb. Log. 64, 53-67 (1999; Zbl 0937.03065)]. Since the proof-theoretic ordinal of EMU is larger than the Feferman-Schütte ordinal \(\Gamma_0\), EMU is not considered as strictly predicative. On the other hand, the proof-theoretic analysis of EMU is carried out by purely predicative methods. This phenomenon has been called `metapredicativity' by G. Jäger, which explains the title of the paper under review. For the entire collection see [Zbl 0919.00040].