Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms (Q5957853)

The paper under review is concerned with Feferman's framework of explicit mathematics. In particular, extensions of his famous theory \(\text{T}_0\) are considered, which provide explicit formulations of inaccessibility and Mahloness. The central concept used to formalize these higher notions of reflection is the one of a \textit{universe}, which can be considered as a collection of types which is closed under previously recognized type existence principles. The paper discusses a novel approach for constructing recursion-theoretic models of \(\text{T}_0\) and its extensions by the limit and Mahlo axioms, thus providing proof-theoretic upper bounds for these systems. The key tool used are the first-order theories for nonmonotone inductive definitions introduced and analyzed in [\textit{G.~Jäger}, J.~Symb. Log. 66, 1073-1089 (2001; Zbl 0989.03064)]. The specific nonmonotone inductive definitions corresponding to recursive inaccessibility and Mahloness are certain combined operator forms due to Richter. Summing up, the authors offer a very natural approach for constructing models of (strong) systems of explicit mathematics, which brings out very clearly the relationship between reflection principles in explicit mathematics and notions of nonmonotone inductive definability.