2.1 $\mathsf {ZFC}$ without Power Set

We will frequently mention $\mathsf {ZFC}$ without Power Set, denoted $\mathsf {ZFC}^-$ . However, $\mathsf {ZFC}^-$ is not obtained by just dropping Power Set from $\mathsf {ZFC}$ :

Note that using Collection instead of Replacement is necessary to avoid pathologies. See [Reference Gitman, Hamkins and Johnstone23] for the details. It is also known by [Reference Friedman, Gitman and Kanovei17] that $\mathsf {ZFC}^-$ does not prove the reflection principle.

2.2 Intuitionistic set theory $\mathsf {IZF}$ and constructive set theory $\mathsf {CZF}$

There are two possible constructive formulations of $\mathsf {ZF}$ , namely $\mathsf {IZF}$ and $\mathsf {CZF}$ , although we will focus on the latter.

$\mathsf {IZF}$ appeared first in H. Friedman’s paper [Reference Friedman15] on the double-negation of set theory. Friedman introduced $\mathsf {IZF}$ as an intuitionistic counterpart of $\mathsf {ZF}$ and showed that there is a double-negation translation from $\mathsf {ZF}$ to $\mathsf {IZF}$ , analogous to that from $\mathsf {PA}$ to $\mathsf {HA}$ .

Constructive Zermelo–Fraenkel set theory, $\mathsf {CZF}$ , is introduced by Aczel [Reference Aczel1] with his type-theoretic interpretation of $\mathsf {CZF}$ . We will introduce subtheories called Basic Constructive Set Theory, $\mathsf {BCST}$ , and $\mathsf {CZF}^-$ before defining the full $\mathsf {CZF}$ .

Definition 2.4. $\mathsf {BCST}$ is the theory that consists of Extensionality, Pairing, Union, Emptyset, Replacement, and $\Delta _0$ -Separation. $\mathsf {CZF}^-$ is obtained by adding the following axioms to $\mathsf {BCST}$ : Infinity, Set Induction, and Strong Collection that states the following: if $\phi (x,y)$ is a formula such that for given a, if $\forall x\in a\exists y \phi (x,y)$ , then we can find b such that

$$ \begin{align*} \forall x\in a\exists y \in b \phi(x,y) \land \forall y\in b\exists x\in a \phi(x,y). \end{align*} $$

We also provide notation for frequently mentioned axioms:

The combination of Full Separation and Collection proves Strong Collection, but the implication does not hold if we weaken Full Separation to $\Delta _0$ -Separation. It is also known that $\Delta _0$ -Separation is equivalent to the existence of the intersection of two sets. See Section 9.5 of [Reference Aczel and Rathjen6] for its proof.

It is convenient to introduce the notion of multi-valued function to describe the Strong Collection and Subset Collection axioms that we will discuss shortly. Let A and B be classes. A relation $R\subseteq A\times B$ is a multi-valued function from A to B if $\operatorname {dom} R=A$ . In this case, we write $R\colon A\rightrightarrows B$ . We use the notation if both $R \colon A\rightrightarrows B$ and $R \colon B\rightrightarrows A$ hold. The reader is kept in mind that the previous definition must be rephrased in an appropriate first-order form if one of A, B, or R is a (definable) proper class in the same way as how we translate classes over $\mathsf {ZF}$ .

Then we can rephrase Strong Collection as follows: for every set a and a class multi-valued function $R \colon \text {a}\rightrightarrows V$ , there is an ‘image’ b of a under R, that is, a set b such that .

Now we can state the Axiom of Subset Collection:

Definition 2.7. The Axiom of Subset Collection states the following: Assume that $\phi (x,y,u)$ is a formula that defines a collection of multi-valued functions from a to b parametrized by $u\in V$ : that is, $\phi (x,y,u)$ satisfies $\forall u \forall x\in a\exists y\in b \phi (x,y,u)$ . Then we can find a set c such that

$$ \begin{align*} \forall u \exists d\in c [\forall x\in a\exists y\in d \phi(x,y,u) \land \forall y\in d\exists x\in a \phi(x,y,u)]. \end{align*} $$

$\mathsf {CZF}$ is the theory obtained by adding Subset Collection to $\mathsf {CZF}^-$ .

We may state Subset Collection informally as follows: for every first-order definable collection of multi-valued class functions $\langle R_u \colon a\rightrightarrows b \mid u\in V\rangle $ from a to b, we can find a set c of all ‘images’ of a under some $R_u$ . That is, for every $u\in V$ there is $d\in c$ such that .

There is a simpler axiom equivalent to Subset Collection, known as Fullness, which is a bit easier to understand.

Then the following hold:

We will not provide a proof for the above proposition, but the reader may consult with [Reference Aczel and Rathjen5] or [Reference Aczel and Rathjen6] for its proof. We also note here that [Reference Rathjen45] showed that Subset Collection does not increase the proof-theoretic strength of $\mathsf {CZF}^-$ , while [Reference Rathjen51] showed that the Axiom of Power Set does.

The following lemma is useful to establish (1) of Proposition 2.9, and is also useful to treat multi-valued functions in general:

Lemma 2.10. Let $R \colon A\rightrightarrows B$ be a multi-valued function. Define $\mathcal {A}(R) \colon A\rightrightarrows A\times B$ by

$$ \begin{align*} \mathcal{A}(R) = \{\langle a,\langle a,b\rangle\rangle \mid \langle a,b\rangle \in R\}. \end{align*} $$

For $S\subseteq A\times B$ , let $\mathcal {A}^S(R) = \{ \langle a, \langle a, b \rangle \rangle | \langle a, b \rangle \in R \cap S\}$ .Footnote ⁵ Then $:$

1. 1. ${\mathcal {A}^S(R)} \colon A\rightrightarrows S \iff R\cap S \colon A\rightrightarrows B$ ,

2. 2. ${\mathcal {A}^S(R)} \colon A\leftleftarrows S\iff S\subseteq R$ .

Proof For the first statement, observe that $\mathcal {A}^S(R) \colon A\rightrightarrows S$ is equivalent to

$$ \begin{align*} \forall a\in A \exists s\in S [\langle a,s\rangle \in \mathcal{A}^S(R)]. \end{align*} $$

By the definition of $\mathcal {A}^S$ , this is equivalent to

$$ \begin{align*} \forall a\in A \exists s\in S [\exists b\in B ( s=\langle a,b\rangle \land \langle a,b\rangle\in R\cap S)]. \end{align*} $$

We can see that the above statement is equivalent to $\forall a\in A\exists b\in B [\langle a,b\rangle \in R\cap S]$ , which is the definition of $R\cap S \colon A\rightrightarrows B$ . For the second claim, observe that $\mathcal {A}^S(R) \colon A\leftleftarrows S$ is equivalent to

$$ \begin{align*} \forall s\in S \exists a\in A [\langle a,s\rangle \in \mathcal{A}^S(R)]. \end{align*} $$

By rewriting $\mathcal {A}^S$ to its definition, we have

$$ \begin{align*} \forall s\in S \exists a\in A [\exists b\in B ( s=\langle a,b\rangle \in R\cap S)]. \end{align*} $$

We can see that it is equivalent to $S\subseteq R$ .

The following lemma is useful when we work with multi-valued functions because it allows us to replace class multi-valued functions over A with set multi-valued functions in A:

It is known that every theorem of $\mathsf {CZF}$ is also provable in $\mathsf {IZF}$ . Moreover, $\mathsf {IZF}$ is quite strong in the sense that its proof-theoretic strength is the same as that of $\mathsf {ZF}$ . On the other hand, it is known that the proof-theoretic strength of $\mathsf {CZF}$ is equal to that of Kripke–Platek set theory $\mathsf {KP}$ . $\mathsf {IZF}$ is deemed to be impredicative due to the presence of Full Separation and Power Set.Footnote ⁷ On the other hand, $\mathsf {CZF}$ is viewed as predicative since it allows for a type-theoretic interpretation such as the one given by Aczel [Reference Aczel1]. However, adding the full law of excluded middle to $\mathsf {IZF}$ or $\mathsf {CZF}$ results in the same theory, namely $\mathsf {ZF}$ .

2.3 Kripke–Platek set theory

Kripke–Platek set theory is the natural intermediate theory between arithmetic and stronger set theories like $\mathsf {ZF}$ . $\mathsf {KP}$ has a natural intuitionistic counterpart called Intuitionistic Kripke–Platek, which we denote by $\mathsf {IKP}$ .

Finally, let us observe that $\mathsf {IKP}$ proves Collection for a broader class of formulas named $\Sigma $ -formulas:

Theorem 2.15. For every $\Sigma $ -formula $\varphi (x, y, u)$ the following is a theorem of $\mathsf {IKP}$ : For every set u, if $\forall x \in a \exists y \varphi (x, y, u)$ then there is a set b such that

$$\begin{align*}\forall x \in a \exists y \in b \varphi(x, y, u) \land \forall y \in b \exists x \in a \varphi(x, y, u). \end{align*}$$

We refer the reader to Section 19 of [Reference Aczel and Rathjen6] or Section 11 of [Reference Aczel and Rathjen5] for some of the basic axiomatic consequences of $\mathsf {IKP}$ and their proofs.

2.4 Inductive definition

Various recursive constructions on $\mathsf {CZF}$ are given by inductive definitions. The reader might refer to [Reference Aczel and Rathjen5] or [Reference Aczel and Rathjen6] to see general information about the inductive definition, but we will review some of the details for the reader who are not familiar with it.

We may think of $\Phi $ as a generalization of a deductive system, and $\Gamma _\Phi (C)$ as a class of theorems derivable from the class of axioms C. Some authors use the notation $X\vdash _\Phi a$ or $X/a\in \Phi $ instead of $\langle X,a\rangle \in \Phi $ . The following theorem says each inductive definition induces a least fixed point:

The following lemma is the essential tool for the proof of the Class Inductive Definition Theorem. See Lemma 12.1.2 of [Reference Aczel and Rathjen6] for its proof:

2.5 Constructive L

In this subsection, we will define the constructible universe L and discuss its properties over $\mathsf {IKP}$ .

Constructing L under a constructive manner was first studied by Lubarsky [Reference Lubarsky35]. Lubarsky developed the properties of L over $\mathsf {IZF}$ , and showed that $\mathsf {IZF}$ proves L satisfies $\mathsf {IZF}$ plus $V=L$ . Crosilla [Reference Crosilla14] showed that the construction of L carries over to $\mathsf {IKP}$ Footnote ⁸ .

There are at least two ways of defining L: the first is using definability over a set model, which Lubarsky [Reference Lubarsky35] and Crosilla [Reference Crosilla14] had taken. Another one is using fundamental operations, also called Gödel operations in the classical context, which was taken by the second author in [Reference Matthews38]. We will follow the second method.

The following lemma says that we can represent every $\Delta _0$ -formula in terms of fundamental operations:

Lemma 2.20 [Reference Matthews38, Lemma 5.2.4], $\mathsf {IKP}$ .

Let $\phi (x_1,\ldots , x_n)$ be a bounded formula whose free variables are all expressed. Then there is a term $\mathcal {F}_\phi $ built up from fundamental operations such that

$$ \begin{align*} \mathsf{IKP}\vdash \mathcal{F}_\phi(a_1,\ldots,a_n) = \{\langle x_n,\ldots,x_1\rangle\in a_n\times\cdots\times a_1\mid\phi(x_1,\ldots,x_n)\}. \end{align*} $$

Then we have the following properties of the constructible hierarchy:

Moreover we can see that $\mathsf {IKP}$ proves L is a model of $\mathsf {IKP}$ :

We will not examine its proof in detail, but it is still worthwhile to mention relevant notions that are necessary for the proof. One of these is hereditary addition, which was first formulated by Lubarsky [Reference Lubarsky35]. This is necessary because $\alpha \in \beta $ does not entail $\alpha +1\in \beta +1$ constructively.

Definition 2.25. For ordinals $\alpha $ and $\gamma $ , define $\alpha +_H\gamma $ by recursion on $\alpha $ :

$$ \begin{align*} \alpha +_H \gamma := \left(\bigcup \{\beta +_H\gamma \mid\beta\in\alpha\}\cup\{\alpha\}\right) + \gamma. \end{align*} $$

Another relevant notion is augmented ordinals. Lubarsky [Reference Lubarsky35] introduced this notion to develop properties of the constructible hierarchy over $\mathsf {IZF}$ . Augmented ordinals are not needed to verify that L is a model of $\mathsf {IKP}$ , but are used to prove the Axiom of Constructibility, and we will use them when working with elementary embeddings.

Definition 2.26. Let $\alpha $ be an ordinal. Then $\alpha $ augmented, $\alpha ^\#$ , is defined recursively on $\alpha $ as

$$ \begin{align*} \alpha^\# := \bigcup\{\beta^\#\mid\beta\in\alpha\}\cup (\omega+1). \end{align*} $$

2.6 Second-order set theories

We need a second-order formulation of constructive set theories in order to define large set axioms corresponding to large cardinals beyond choice. We will formulate constructive analogues of Gödel–Bernays set theory $\mathsf {GB}$ whose first-order counterparts are $\mathsf {CZF}$ and $\mathsf {IZF}$ , respectively. We will use $\forall ^0$ and $\exists ^0$ for quantifications over sets, and $\forall ^1$ and $\exists ^1$ for quantifications over classes. We omit the superscript if the context is clear. Following standard conventions, we will use uppercase letters for classes and lowercase letters for sets, unless specified otherwise. The reader could consult with [Reference Williams64] if they are interested in classical second-order set theory.

Remark 2.30. We do not need to add the Class Subset Collection axiom

asFootnote ⁹ an axiom of $\mathsf {CGB}$ because it is derivable from the current formulation of $\mathsf {CGB}$ : we can prove it from the first-order Fullness and the Class Strong Collection by mimicking the proof of Set Collection from Fullness and Strong Collection.

The reader should also note that, unlike classical $\mathsf {GB}$ , there is no additional Separation axiom for sets: that is, we do not assume $a{\kern-1pt}\cap{\kern-1pt} A{\kern-1pt}={\kern-1pt}\{x{\kern-1pt}\in{\kern-1pt} a {\kern-1pt}\mid{\kern-1pt} x{\kern-1pt}\in{\kern-1pt} A\}$ is a set for a given class A. In fact, the assumption that $a\cap A$ is always a set implies Full Separation due to Elementary Comprehension.

Thus we introduce a new terminology for classes such that $A\cap a$ is always a set:

The following lemma shows every class function is amenable:

Next, we define the second-order variant of $\mathsf {IZF}$ which we denote by $\mathsf {IGB}$ . $\mathsf {IGB}$ allows Separation for arbitrary classes as classical $\mathsf {GB}$ does.

We know that classical $\mathsf {GB}$ is a conservative extension of $\mathsf {ZF}$ . We expect the same results to hold for constructive set theories. The following theorem shows it actually holds; however, its proof will require a small amount of proof theory. We borrow ideas of the proof from [63].

2.7 Second-order set theories with infinite connectives

We will use infinite conjunctions to circumvent technical issues about defining elementary embeddings. Hence we define an appropriate infinitary logic and the corresponding second-order set theories. The following definition appears in [Reference Negri43]:

Definition 2.35 ( $\mathsf {G3i_\omega }$ [Reference Negri43]).

The intuitionistic cut-free first-order sequent calculus $\mathsf {G3i_\omega }$ is defined by the following rules: initial sequents are of the form $P,\Gamma \implies \Delta ,P$ and its deduction rules are:

The difference between finitary logic and $\mathsf {G3i}_\omega $ is that the latter allows for infinite conjunctions and disjunctions over countable sets of formulas. This will only be needed in order to formalise the concepts of Super Reinhardt sets and the total Reinhardtness of V in Section 4.2. Otherwise, throughout this paper, we will stick to finitary logic.

It is well-known that the usual classical and intuitionistic predicate calculus enjoys the cut-elimination rule. This is the same for $\mathsf {G3i_\omega }$ . We state the following proposition without proof. The reader might refer to [Reference Negri43] for its proof.

Finally, we are ready to define set theories over $\mathsf {G3i_\omega }$ :

Note that the infinitary logic $\mathsf {G3i_\omega }$ has no role in defining new sets from the given sets: for example, we do not have Separation schemes for infinite conjunctions and disjunctions. The only reason we are using $\mathsf {G3i}$ is to enhance the expressive power of set theories as we introduced classes into first-order set theories. The following theorem shows that infinite connectives do not provide new theorems into $\mathsf {CGB}$ or $\mathsf {IGB}$ :

4.1 Critical sets and Reinhardt sets

In this section, we will give the basic tools that we shall need to work with elementary embeddings. When working with some embedding $j \colon V \rightarrow M$ we will not in general be assumed that either j or M is definable in a first-order manner. This means that we cannot state Collection or Separation for formulas involving j or M in a purely first-order way. Therefore, to deal with them, we will need to expand our base theory to accommodate class parameters. This leads to the following convention, whose main purpose is to simplify later notation.

We begin with the weak theory of the Basic Theory of Elementary Embeddings, originally introduced by Corazza in [Reference Corazza13]. This is the minimal theory required to state that $j \colon V \rightarrow V$ is an elementary embedding with a critical point but without assuming anything about the relevant Separation, Collection, or Set Induction schemes over the extended language. For our purposes, it will in fact be beneficial to weaken this further to $\mathsf {BTEE}_M$ which is the minimal theory stating that $j \colon V \rightarrow M$ is an elementary embedding with a critical point for some $M \subseteq V$ .

We shall see in Section 5 that $\mathsf {IKP}_j$ with a critical point implies the consistency of $\mathsf {IZF + BTEE}$ and in Section 6 that the latter is equiconsistent with $\mathsf {ZF} + \mathsf {BTEE}$ , which already has a quite high consistency strength.

Classically, $\mathsf {BTEE}$ is a relatively weak principle which is implied by the large cardinal axiom $0^\#$ , which is the statement that there is a non-trivial elementary embedding $j \colon L \rightarrow L$ . The reason this is weak is because we do not have Separation in the extended language which means that we cannot produce sets of the form $j \operatorname {\mathrm {\upharpoonright }} a$ for arbitrary sets a.

Over $\mathsf {IKP}_j$ , being a critical point of an elementary embedding is sufficient to prove some of the basic properties one would want from the theory of elementary embeddings. For example, one can show that if there is a critical point then there is (at least one) critical point which is an ordinal (see Chapter 9 of [Reference Ziegler67] or Chapter 7 of [Reference Matthews38] for details) or that there is a model of (first-order) $\mathsf {IZF}$ .

However, such an assumption is not necessarily the most natural counterpart to the classical notion of non-trivial elementary embeddings. For example, consider $\mathsf {ZFC}$ plus an elementary embedding $j \colon V \rightarrow M$ with critical point $\kappa $ . Then $L_\kappa $ can easily be seen to be a critical point as defined above; however, it is the ‘wrong’ set to work within this context because it is not a model of second-order $\mathsf {ZFC}$ . In particular, one can show that $\mathcal {P}(\omega )^L$ is merely a countable set. Instead, what one wants to work with is a critical point which is an inaccessible set, and this is what we shall define next. Note that in weak theories there is no reason that having a critical point will imply the existence of such a set. For example, it is proven in Chapter 10 of [Reference Matthews38] that it is possible to produce a model of $\mathsf {ZFC}^-$ with a non-trivial elementary embedding, while also having that $\mathcal {P}(\omega )$ is a proper class, and in such a model there will be no set sized models of second-order $\mathsf {ZFC}^-$ .

Now let us define critical sets and Reinhardt sets in terms of elementary embeddings:

We introduce one final definition which is intermediate between $\mathsf {BTEE}$ and Reinhardt sets; the Wholeness Axiom. This was first formulated by Corazza [Reference Corazza12] and later stratified by Hamkins [Reference Hamkins28] in order to investigate what theory was necessary to produce the Kunen Inconsistency under $\mathsf {ZFC}$ .

We will use the term critical point and critical set simultaneously, so the reader should distinguish the difference between these two terms. (For example, a critical point need not be a critical set unless it is inaccessible.) Note that the definition of critical sets is different from that suggested by Hayut and Karagila [Reference Hayut and Karagila29]: they defined a critical cardinal as a critical point of an elementary embedding $j \colon V_{\kappa +1}\to M$ for some transitive set M. This is done to ensure that the embedding j is a set and therefore first-order definable. We will instead take the more natural, but not obviously first-order definable, definition where the domain is taken to be the universe, which is what Schlutzenberg calls V-critical in [Reference Schlutzenberg58]. Finding and analyzing the $\mathsf {CZF}$ -definition of a critical set that is classically equivalent to a critical set in the style of Hayut and Karagila would be good future work. Also, [Reference Ziegler67] uses the term ‘measurable sets’ to denote critical sets, but we will avoid this term for the following reasons: it does not reflect that the definition is given by an elementary embedding, and it could be confusing with measurable sets in measure theory.

We do not know if every elementary embedding $j \colon V\to M$ over $\mathsf {CZF}$ enjoys being cofinal. Surprisingly, the following lemma shows that j becomes a cofinal map if $M=V$ . Note that the following lemma heavily uses Subset Collection. See Theorem 9.37 of [Reference Ziegler67] for its proof.

Note that [Reference Ziegler67] uses the term set cofinality to denote our notion of cofinality. However, we will use the term cofinality to harmonize the terminology with that of [Reference Matthews39]. Ziegler’s theorem on the cofinality of Reinhardt embedding was an early indication of the high consistency strength of $\mathsf {CZF}$ with a Reinhardt set. This is because [Reference Matthews39] shows that a related weak set theory, namely $\mathsf {ZFC}^-$ with the $\mathsf {DC}_\mu $ -scheme for all cardinals $\mu $ , already proves there is no cofinal non-trivial elementary embedding $j \colon V\to V$ .

The following lemma, due to Ziegler [Reference Ziegler67], has an essential role in the proof of Proposition 4.8 and developing properties of large large sets. We note here that the proof will not require V to satisfy any of our axioms in the language expanded with j or for the embedding to be fully elementary and therefore the Lemma is also provable over weaker theories such as $\mathsf {IKP + BTEE}$ . Note that, when working without Power Set, $\mathcal {P}(\mathcal {P}(a))$ should be seen as an abbreviation for the class consisting of those sets whose elements are all subsets of a.

4.2 Large set axioms beyond choice

As before, there is no reason why we should stop at Reinhardt sets. While Reinhardt cardinals are incompatible with $\mathsf {ZFC}$ , it is known that all proofs of this use the Axiom of Choice in an essential way. This has led to the study of stronger large cardinals in the $\mathsf {ZF}$ context, the most notable example being [Reference Bagaria, Koellner and Woodin10]. We will focus on the concept of super Reinhardt sets and totally Reinhardt sets. However, before we do so, we note a technical difficultly regarding truth predicates and first-order definability, which is why we will need to work in an infinitary second-order theory.

Using [Reference Gaifman18, Theorem 1] or [Reference Kanamori33, Proposition 5.1], in $\mathsf {ZF}$ , an elementary map $j \colon V\to M$ is fully elementary if it is $\Sigma _1$ -elementary. Unfortunately, in our context, we do not know whether $\Sigma _n$ -elementary embeddings are fully elementary even if n is sufficiently large.

During this subsection, we will fix an enumeration $\langle \phi _{n}(X,\vec {x})\mid n\in \mathbb {N}\rangle $ of all first-order formulas over the language of set theory with one class variable X.

The reader should notice that we have formulated critical sets and Reinhardt sets over $T_{j,M}$ where T was some general, unspecified (first-order) theory, whereas the definition of super Reinhardt sets in formulated in the specified second-order theory of $\mathsf {CGB}_\infty $ . Some readers could think that formulating criticalness and Reinhardtness over $\mathsf {CGB}_\infty $ would be more natural, as Bagaria–Koellner–Woodin formulated Reinhardt cardinals over $\mathsf {GB}$ instead of $\mathsf {ZF}_j$ . It will turn out that sticking to the more first-order formulation of criticalness and Reinhardtness is better for the following technical reason. We will take a double-negation interpretation based on Gambino’s Heyting-valued interpretation [Reference Gambino20] over first-order constructive set theories in Section 6. It is harder to extend Gambino’s interpretation to a second-order set theory than extending it to $\mathsf {CZF}_{j,M}$ because the former requires extending Gambino’s forcing to all classes and defining the interpretation of second-order quantifiers, while the latter does not. However, we cannot avoid the full second-order formulation of super Reinhardtness, unlike we did for Reinhardtness, because its definition asks for class many elementary embeddings.

Our definition of A-super Reinhardtness is different from that of Bagaria–Koellner–Woodin [Reference Bagaria, Koellner and Woodin10] because they required j to satisfy $j^+[A] :=\bigcup _{x\in V} j(A\cap x)$ is equal to A instead of A-elementarity. It turns out by Lemma 4.14 that our definition is stronger than that of Bagaria–Koellner–Woodin in our constructive context, but they are equivalent in the classical context.

Lemma 4.12 ( $\mathsf {CGB}$ ).

Let $\phi (X, x_0,\ldots , x_n)$ be a $\Delta ^X_0$ -formula whose free variables are all expressed. If A is an amenable class and if we take $a = \operatorname {TC}(\{x_0,\ldots ,x_n\})$ , then

$$ \begin{align*}\phi(A,x_0,\ldots,x_n) \leftrightarrow \phi(A\cap a,x_0,\ldots, x_n).\end{align*} $$

The upshot of the second claim in the above lemma is that $\mathsf {GB}$ proves that given a fully elementary embedding, it is A-elementary if it is $\Delta ^A_0$ -elementary. Furthermore, the condition $j^+[A]=A$ is equivalent to $\Delta ^A_0$ -elementarity. Hence Lemma 4.14 justifies that our definition of super Reinhardtness is a reasonable constructive formulation of that of Bagaria–Koellner–Woodin.

We also note here that we can weaken the assumption in the second clause of Lemma 4.14: namely, $\mathsf {GB}$ proves every cofinal $\Delta ^A_0$ -elementary embedding $j\colon V\to V$ is fully elementary for A-formulas.

We end this section with one final large set axiom which we will see suffices to bring the constructive theory into proof-theoretic equilibrium with its classical counterpart.

5.1 The strength of elementary embeddings over $\mathsf {BTEE}_M$

The aim of this subsection is to derive a lower bound for the consistency strength of an elementary embedding $j\colon V\to M$ with a critical point. One amazing consequence of Lemma 4.9 is that the existence of a critical set is already quite strong, compared to small large set axioms over $\mathsf {CZF}$ . As in the lemma, we remark here that we do not require V to satisfy any axiom in the expanded language and therefore the proof also works over $\mathsf {IKP} + \Delta _0\text {-} \mathsf {BTEE}_M$ .

Hence the existence of an elementary embedding with a critical point is already tremendously strong compared to $\mathsf {CZF}$ . We will see in Section 6 that $\mathsf {IZF}$ interprets classical $\mathsf {ZF}$ , so the existence of a critical set over $\mathsf {CZF}$ is stronger than $\mathsf {ZF}$ . However, it turns out that the hypotheses given in Theorem 5.1 proves the critical point K satisfies not only $\mathsf {IZF}$ , but also large set axioms. For example, we next show that K is a model of $\mathsf {IZF+pIEA}$ . The proof begins with the following lemmas:

Proof We proved that K is a model of $\mathsf {IZF}$ and $\mathcal {P}(a) \cap K = \mathcal {P}(a) \cap j(K)$ for any $a \in K$ . Thus it suffices to show that $j(K)$ believes K is regular. That is,

The proof employs basically the same argument as the proof that K satisfies Collection given in Theorem 5.1: let $a\in K$ , $R\in j(K)$ , and suppose that $R\colon a\rightrightarrows K$ . Then

$$ \begin{align*} V\models R: a\rightrightarrows K ~ \implies ~ M\models j(R): a\rightrightarrows j(K). \end{align*} $$

Now let $b=\{y\in K \mid \exists x\in a \ \langle x,y\rangle \in j(R)\}\in M$ . Since b is a subset of $K\in j(K)$ , we have $b\in j(K)$ . Furthermore, b witnesses . Hence, by elementarity, there exists $b \in K$ such that .

Proof By Lemma 5.2, $j(K)$ believes K is power inaccessible. Fix $a\in K$ , then $b=K$ witnesses the following statement:

$$ \begin{align*} M \models \big[ \exists b\in j(K) \big( a\in b \land j(K)\models b\ \text{is power inaccessible} \big) \big]. \end{align*} $$

Hence by elementarity, there is $b\in K$ such that $a\in b$ and K believes b is power inaccessible. Since a is arbitrary, we have $K \models \mathsf {IZF + pIEA}$ .

In fact, we can derive more: we can show that not only does K satisfy $\mathsf {pIEA}$ , but K also satisfies $\forall x\exists y[x\in y\land \Phi (y)]$ , where $\Phi $ is any large set properties such that $j(K) \models \Phi (K)$ . Especially, $\Phi $ can be a combination of power inaccessibility with Mahloness or 2-strongness. (See [Reference Rathjen46] or [Reference Ziegler67] for the details of Mahlo sets or 2-strong sets.)

5.2 Iterating j to a critical point

In the classical context, one usually works with $\lambda =j^\omega (\kappa )=\sup _{n<\omega }j^n(\kappa )$ for $\kappa =\operatorname {crit} j$ when they study large cardinals at the level of rank-into-rank embeddings and beyond. We can see in the classical context that if $j\colon V\to M$ is elementary embedding with $\kappa =\operatorname {crit} j$ , then $V_\lambda $ is still a model of $\mathsf {ZFC}$ with some large cardinal properties.

We may expect the same in a constructive manner, but defining the analogue of $\lambda =j^\omega (\kappa )$ cannot be done over $\mathsf {IKP}+\Sigma \text {-} \mathsf {BTEE}_M$ . The problem is that the definition of $\lambda $ requires defining $\langle j^n(\kappa ) \mid n\in \omega \rangle $ , which requires recursion for j-formulas. It turns out that we can define this sequence if we have Set Induction for $\Sigma ^{j, M}$ -formulas. Moreover, even if we have this sequence, we require an instance of $\Sigma ^{j, M}$ -Replacement to turn the sequence into a set, which is when we will have to start working in $\mathsf {IKP}_{j,M}$ .

Definition 5.5 ( $\mathsf {IKP}+\Sigma \text {-} \mathsf {BTEE}_M$ ).

Let $j\colon V\to M$ be an elementary embedding with a critical point K. Following Corazza [Reference Corazza13, (2.7)–(2.9)], let $\Theta $ and $\Phi $ be the following formulas:

$$ \begin{align*} \Theta(f,n,x,y) & \equiv f \text{is a function}\land \operatorname{dom} f = n+1 \land f(0) = x \, \land \\ &\forall i \big( 0<i\le n\to f(i) = j(f(i-1)) \land f(n) = y\big),\\ \Phi(n,x,y) & \equiv n\in\omega \to \exists f\ \Theta (f,n,x,y). \end{align*} $$

Informally speaking, $\Theta (f,n,x,y)$ states that f is a function with domain $n + 1$ computing $j^n(x)=y$ , and $\Phi (n,x,y)$ asserts that $j^n(x)=y$ . We can see that $\Theta $ is $\Delta ^{j,M}_0$ and $\Phi $ is $\Sigma ^{j,M}$ . A careful analysis will show that $\Phi $ allows a $\Pi ^{j,M}$ -formulation, so $\Phi $ is actually $\Delta ^{j,M}$ . However, this fact is irrelevant in our context.

Hence we can define the constructive analogue of $\lambda =j^\omega (\kappa )$ , by using an instance of $\Sigma ^{j,M}$ -Replacement:

Now we can see that K is an elementary submodel of $\Lambda $ :

Lemma 5.11 ( $\mathsf {IKP}_{j,M}$ ).

Let $j \colon V\to M$ be an $\Delta _0$ -elementary embedding with a critical point K, and assume that $K\models \Delta _0\text {-} \mathsf {Sep}$ . Then K is an elementary submodel of $\Lambda $ . That is, the following holds $:$ for every formula $\phi (\vec {x})$ (without j or M) all of whose free variable are expressed,

(1) $$ \begin{align} V\models \forall \vec{x}\in K [\phi^K(\vec{x})\leftrightarrow \phi^\Lambda(\vec{x})]. \end{align} $$

An upshot of Lemma 5.11 is that $j^n(K)$ is an elementary submodel of  $\Lambda $ .Footnote ¹² Especially, by applying this fact to Lemma 5.3, we have:

Especially, we have an analogue of Lemma 5.2 between K and $\Lambda $ :

As a corollary of the previous results, we have:

5.3 Playing with a $\Sigma $ - $\mathrm {Ord}$ -inary elementary embedding over $\mathsf {IKP}$

Let us examine what we can derive from a $\Sigma $ -elementary embedding with an ordinal critical point. An illuminating result along this line is that of Ziegler [Reference Ziegler67], which is proved by considering the rank of any fixed critical point K: