Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe (Q1861330)

The paper contributes to the investigation of proof-theoretic problems, which involve the comparison of three different formal frameworks relevant to the foundations of constructive mathematics: Martin-Löf's type theories, Feferman's explicit mathematics, constructive set theories (Myhill, Friedman, Aczel). In particular, the paper establishes lower bounds on the strength of Feferman's system T\(_0\) for explicit mathematics, expanded with axioms M and M\(^+\) (respectively) implying (suitable forms of) Mahlo principles. It has to be noticed that in this area of proof theory lower bound results are often established by means of well-ordering proofs. Yet the author follows a different route: he is able to embed Aczel's constructive set theories extended with corresponding set-theoretic Mahlo principles -- to be named CZFM and CZFM\(^+\) -- into \(T_0+\text{M}\) and and \(T_0+\text{M}^+\) (respectively). As usual, Aczel's CZF includes (in the language of set theory) extensionality, foundation, union, pair, bounded separation, a strong form of collection, subset collection, infinity. Concerning the axioms of \(T_0\), they include axioms for partial extended combinatory logic, natural numbers, elementary comprehension, join (i.e. uniform disjoint sum) and inductive generation (there is an operation \(i\) picking out uniformly of any pair \(\alpha\), \( \beta\) of classes the class \(i(\alpha,\beta)\), representing the largest well-founded part of \(\alpha\) with respect to the relation encoded by \(\beta\)). As to Mahloness, the first principle -- called M -- states that (i) there is an operation \(u\) which associates to any class \(\alpha\) a universe \(u\alpha\), namely a class of classes, which contains \(\alpha\) and is closed under elementary comprehension and join; (ii) there exists an operation \(m\) such that that, if \(f\) is an operation mapping (non-extensional) classes into themselves, then \(m(f)\) is a universe closed under \(f\). The second principle, \(\text{M}^+\), asserts that there exists a universe M which is closed under \(u\), \(m\) and \(i\). The embedding technique used by Tupailo amounts to a realizability interpretation. The general idea runs as follows: if \(A\) is a statement provable, say, in CZFM, one associates to \(A\) a suitable formula of explicit mathematics \([t\underline{rn}A]\), so that, if \(A\) is provable in CZFM, then \([t\underline{rn}A]\) is provable in \(T_0+ \text{M}\), for some suitable term (encoding witnessing information about \(A\)). To this aim, it is crucial to define a notion of set representative in explicit mathematics by means of suitable well-founded trees; and the soundness of the construction requires a lot of verifications and non-trivial work. The main result can also be regarded as an extension of the preparatory results by the same author [J. Symb. Log. 66, 1848-1864 (2001; Zbl 0993.03075)]. There it was shown that subsystems of second-order arithmetic of strength at most \(\Delta^1_2\)-CA+BI are reducible via realizability techniques to \(T_0\) (recall that by work of Jäger and Pohlers \(\Delta^1_2\)-CA+BI is proof-theoretically equivalent to \(T_0\)). A pleasant outcome of the paper is that, up to a certain point, there is a perfect intuitive match between higher reflection principles in constructive set theory and universe properties in explicit mathematics. As we already mentioned, the work is technical in nature and it requires several detailed verifications; but we find it clearly written and enough motivated at crucial points.