Very large set axioms over constructive set theories

TL;DR

This paper explores large set axioms based on elementary embeddings in constructive set theories, showing they can reach the strength of classical set theories like ZFC and surpass certain large cardinal axioms.

Contribution

It introduces new large set axioms via elementary embeddings in constructive set theories and analyzes their proof-theoretic strength, revealing they can match or exceed classical set theory strengths.

Findings

Adding elementary embedding properties to IKP yields ZFC consistency.

Reinhardt sets have greater consistency strength than ZF+WA.

Super Reinhardt sets and TR exceed ZF with large cardinals.

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 $\mathsf{\Delta_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.