Universes in explicit mathematics (Q5939842)

The paper investigates the proof-theoretic strength of systems of explicit mathematics (in the sense ot S. Feferman) with universes, i.e. collections of objects satisfying certain strong closure conditions. In the framework of explicit mathematics, a universe is a type \(U\) such that \(U\) is closed under elementary comprehension and join and all elements of \(U\) are so-called names. The paper gives a comprehensive treatment of various aspects of universes in systems of explicit mathematics. In particular, limit axioms, least universes and name induction are studied. Various systems based on these principles are shown to have the same proof-theoretic strength as the well-known system \(T_0\) from \textit{S. Feferman}'s pioneering paper ``A language and axioms for explicit mathematics'' [Lect. Notes Math. 450, 87-139 (1975; Zbl 0357.02029)].