Reflections on reflections in explicit mathematics

DOI10.1016/J.APAL.2005.05.008MaRDI QIDQ2566068zbMATH OpenOpenAlexFDO

Publication date 22 September 2005

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2005.05.008

2-universe axiom explicit mathematics reflection principles survey

Nonclassical and second-order set theories (03E70) Recursive ordinals and ordinal notations (03F15) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Review text

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.

Recommendations

Cites work

Cited in

(15)

This page was built for publication: Reflections on reflections in explicit mathematics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2566068)