Reflections on reflections in explicit mathematics (Q2566068)

This is an excellent survey of the effect of reflection principles on explicit mathematics and similar constructive systems. The authors take up three successively stronger principles: the limit axiom, the Mahlo axiom, and the 2-universe axiom. They compare the strengths of various systems and their proof-theoretic ordinals. The results about the 2-universe axiom are new, and the authors' account is a delight. They exhibit a naïve approach first, point out difficulties it encounters, then show how to modify it, and sketch the proof of ``EU+(2-uni) is equivalent to KPi\(^0\)+(\(\Pi_3\)-Ref), and their ordinal is \(\Theta\Omega^\omega 0\)'', and the like. (They further point out the possibility of extending to \(n\)-universes and so on.) The authors begin this paper with historical and motivational accounts, then display (formal) languages including symbols and axioms to be used, with short explanations. They also explain relevant subjects like admissible set theories [e.g. KPi], and the \(n\)-ary Veblen function, which is a natural generalization of the ordinary binary one. Throughout the paper an abundant guide to the relevant literature is given.