
arXiv: 2204.05831
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.
Large cardinals, Primary 03E70, Secondary 03E55, large set axioms, Nonclassical and second-order set theories, consistency strength, FOS: Mathematics, constructive set theory, Mathematics - Logic, elementary embedding, Logic (math.LO)
Large cardinals, Primary 03E70, Secondary 03E55, large set axioms, Nonclassical and second-order set theories, consistency strength, FOS: Mathematics, constructive set theory, Mathematics - Logic, elementary embedding, Logic (math.LO)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 2 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
