VERY LARGE SET AXIOMS OVER CONSTRUCTIVE SET THEORIES
Hanul Jeon, RICHARD MATTHEWS · Bulletin of Symbolic Logic · 2024
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 $\Delta _0$ -formulas, which we will denote by $\Delta _0\text {-}\mathsf {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.