Very large set axioms over constructive set theories
Hanul Jeon, Richard Matthews
TL;DR
The paper develops a deep integration of large-set axioms into constructive set theories by leveraging elementary embeddings, revealing that even a modest fragment $\Delta_0\text{-}\mathsf{BTEE}_M$ yields strong consistency results surpassing classical second-order arithmetic. It demonstrates that Reinhardt-type and stronger notions (including super Reinhardt and totally Reinhardt) push the constructive strength beyond $\,\mathsf{ZF}$ with choiceless large cardinals, and it develops two-second-order constructive theories $\mathsf{CGB}$ and $\mathsf{IGB}$ to formalize these notions. A key methodological contribution is the use of Gambino’s Heyting-valued interpretation and the double-negation topology to relate constructive and classical theories, enabling the extraction of lower bounds and translation-based conservativity results. The work connects internal strength analyses with external interpretability results and to a broader program of aligning constructive set theories with classical large-cardinal hierarchies, while outlining substantial avenues for future refinement and expansion. Overall, the paper provides foundational tools and results indicating that large-set axioms in a constructive setting can reach consistency strengths comparable to substantial classical large-cardinal frameworks, through carefully crafted embedding-based formulations and second-order mechanisms.
Abstract
We investigate large set axioms defined in terms of elementary embeddings over constructive set theories, focusing on $\mathsf{IKP}$ and $\mathsf{CZF}$. Most previously studied large set axioms, notably the constructive analogues of large cardinals below $0^\sharp$, have proof-theoretic strength weaker than full Second-order Arithmetic. On the other hand, the situation is dramatically different for those defined via elementary embeddings. We show that by adding to $\mathsf{IKP}$ the basic properties of an elementary embedding $j\colon V\to M$ for $Δ_0$-formulas, which we will denote by $\mathsf{Δ_0\text{-}BTEE}_M$, we obtain the consistency of $\mathsf{ZFC}$ and more. We will also see that the consistency strength of a Reinhardt set exceeds that of $\mathsf{ZF+WA}$. Furthermore, we will define super Reinhardt sets and $\mathsf{TR}$, which is a constructive analogue of $V$ being totally Reinhardt, and prove that their proof-theoretic strength exceeds that of $\mathsf{ZF}$ with choiceless large cardinals.