How strong is a Reinhardt set over extensions of CZF?

In Section 2 and 3, we will cover relevant preliminaries. We will review constructive set theory in Section 2 and large set axioms in Section 3, so the readers who are already familiar with these topics may skip them. In Section 4, we review and discuss Gambino’s Heyting-valued interpretation [9] over the double negation formal topology $\Omega$, which is the main tool of the paper. It forces $\mathsf{\Delta_{0}\text{-}LEM}$, the law of excluded middle for bounded formulas. By assuming the Full Separation, we may turn $\mathsf{\Delta_{0}\text{-}LEM}$ to the full law of excluded middle. However, forcing over $\Omega$ does not preserve every axiom of $\mathsf{CZF}$: it does not preserve the Axiom of Subset Collection, a $\mathsf{CZF}$-analogue of Power Set axiom. Thus the resulting theory of forcing over $\Omega$ is $\mathsf{ZF^{-}}$ if we start from $\mathsf{CZF+Sep}$. Unlike ‘small’ formal topologies, $\Omega$ is not absolute between transitive models, and it causes issues about the absoluteness of the Heyting-valued interpretation. We will also discuss it in this section. Section 5 is devoted to prove elementary embeddings are preserved under $\Omega$. However, $\Omega$ does not prove the inaccessibility of a critical point of the elementary embedding, and it restricts the analysis on the consistency strength of $\mathsf{CZF+Sep}$ with an elementary embedding. We will deal with this issue in Section 6 by showing that the Heyting-valued interpretation under $\Omega$ still proves the critical point enjoys a strong reflection principle, which makes the critical point a transitive model of $\mathsf{ZF}$ with large cardinal axioms. We briefly discuss why achieving the upper bound of the consistency strength of our object theories in Section 7, with some concluding questions.

We will frequently mention $\mathsf{ZFC}$ without Power Set, called $\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 [10] for the details. It is also known by [8] that $\mathsf{ZFC^{-}}$ does not prove the reflection principle.

Constructive Zermelo-Fraenkel set theory $\mathsf{CZF}$ is introduced by Aczel [2] 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}$.

We will also define some synonyms for frequently-mentioned axioms:

Full separation proves Strong Collection from Collection, but $\Delta_{0}$-Separation is too weak to do it. It is also known that $\Delta_{0}$-Separation is equivalent to the existence of the intersection of two sets. See Section 9.5 of [4] for its proof.

It is convenient to introduce the notion of multi-valued function to describe Strong Collection and Subset Collection that appears later. 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:A\rightrightarrows B$. We use the notation $R:A\>\mathrlap{\leftleftarrows}{\rightrightarrows}\>B$ if both $R:A\rightrightarrows B$ and $R:B\rightrightarrows A$ hold. Then we can rephrase Strong Collection as follows: for every set $a$ and a class $R:a\rightrightarrows V$, there is a set $b$ such that $R:a\rightrightarrows b$.

Now we can state the Axiom of Subset Collection:

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

Then the following holds:

We do not provide the proof for it, and the readers may consult with [5] or [4] for its proof. Note that Subset Collection does not increase the proof-theoretic strength of $\mathsf{CZF^{-}}$ while the Axiom of Power Set does. The following lemma is useful to establish (1) of subsection 2.2, and is also useful to treat multi-valued functions:

The following lemma provides useful applications of Strong Collection:

Various recursive construction on $\mathsf{CZF}$ is given by inductive definition. The readers might refer [5] or [4] to see general information about inductive definition, but we will review some of it for the readers who are not familiar with it.

We may think $\Phi$ as a generalization of a deductive system, and $\Gamma_{\Phi}(C)$ 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$.

Each Inductive definitions arise the least class fixed point:

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

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

It is known that every theorem of $\mathsf{CZF}$ is that of $\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}$ with Infinity. $\mathsf{IZF}$ is deemed to be impredicative due to the presence of Full Separation and Power Set.¹¹1There is no consensus on the definition on the predicativity. The usual informal description of the predicativity is rejecting self-referencing definitions. On the other hand, $\mathsf{CZF}$ is viewed as predicative since it allows the type-theoretic interpretation given by Aczel [2]. However, adding the full law of excluded middle into $\mathsf{IZF}$ or $\mathsf{CZF}$ results in the same $\mathsf{ZF}$.

The first large set notions over $\mathsf{CZF}$ would be regular sets. Regular sets appear first in Aczel’s paper [3] about inductive definitions over $\mathsf{CZF}$. As we will see later, regular sets can ‘internalize’ most inductive constructions, which turns out to be useful in many practical cases.

There is no ‘pair-closed regular sets’ since every regular set is closed under pairings if it contains 2:

$\mathsf{REA}$ has various consequences: For example, $\mathsf{CZF^{-}+REA}$ proves Subset Collection. Moreover, it also proves that every bounded inductive definition $\Phi$ has a set-sized fixed point $I(\Phi)$.

The notion of regular sets is quite restrictive, as it does not have Separation axioms, at least for $\Delta_{0}$-formulas, so we have no way to do any internal construction over a regular set. The following notion is a strengthening of regular set, which resolves the issue of internal construction:

We do not know that $\mathsf{CZF}$ proves every regular set is BCST-regular, although Lubarsky and Rathjen [20] proved that the set of all hereditarily countable sets in the Feferman-Levy model is functionally regular but not $\bigcup$-regular. It is not even sure that the existence of a regular set implies that of BCST-regular set. However, every inaccessible set is BCST-regular, and every BCST-regular set appearing in this paper is inaccessible.

What are regular sets and inaccessible sets in the classical context? The following result illustrates how these sets look like under the well-known classical context:

Note that we follow the Hayut and Karagila’s definition [14] of inaccessiblity in choiceless context; that is, $\kappa$ is inaccessible if $V_{\kappa}\models\mathsf{ZF_{2}}$.

There is no reason to stop defining large set notions up to weaker ones. Hence we define stronger large set axioms. The main tool to access strong large cardinals (up to measurable cardinals) is to use elementary embedding, so we follow the same strategy:

We will use the term critical point and critical set simultaneously, so the readers should distinguish the difference of 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 apparently stronger than that is suggested by Hayut and Karagila [14]. Finding the $\mathsf{CZF}$-definition of a critical set which is classically equivalent to a critical set in the style of Hayut and Karagila would be a good future work. Also, Ziegler [24] 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 every elementary embedding $j:V\prec M$ over $\mathsf{CZF}$ enjoys cofinal properties. Surprisingly, the following lemma shows that $j$ become a cofinal map if $M=V$, even under $\mathsf{CZF}$ without any assumptions. Note that the following lemma uses Subset Collection heavily. See Theorem 9.37 of [24] for its proof.

Note that Ziegler [24] 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 Matthews [17].

We will follow Gambino’s definition [9] of Heyting-valued interpretation. We start this section by reviewing relevant facts on the Heyting-valued interpretation.

Forcing is a powerful tool to construct a model of set theory. Gambino’s definition of the Heyting-valued model (or alternatively, forcing) opens up a way to produce forcing models of $\mathsf{CZF^{-}}$. His Heyting-valued model starts from formal topology, which formalizes a poset of open sets with a covering relation:

For each formal topology $\mathcal{S}$, we have a notion of nucleus $\jmath p$ given by

Then the class $\operatorname{Low}(\mathcal{S})_{\jmath}$ of all lower subsets²²2A subset $p\subseteq S$ is a lower set if $\downarrow p=p$. that are stable under $\jmath$ (i.e., $\jmath p=p$) form a set-generated frame:

Note that every set-generated frame has every operation of Heyting algebra: for example, we can define $a\to b$ by $a\to b=\bigvee\{x\in g\mid x\land a\leq b\}$, $\bot$ by $\varnothing$, and $\bigwedge p$ by $\bigvee\{x\in g\mid\forall y\in p(x\leq y)\}$.

We extend the nucleus $\jmath$ to general classes by taking $JP:=\bigcup\{\jmath p\mid p\subseteq P\}$, and define operations on classes by $P\land Q=P\cap Q$, $P\lor Q=J(P\cup Q)$ and $P\to Q=\{x\in S\mid x\in P\to x\in Q\}$. For a set-indexed collection of classes $\{P_{x}\mid x\in I\}$, take $\bigwedge_{x\in I}P_{x}=\bigcap_{x\in I}P_{x}$ and $\bigvee_{x\in I}P_{x}=J\left(\bigcup_{x\in I}P_{x}\right)$. Note that $JP=\jmath P$ if $P$ is a set and we have the Full Separation.

The Heyting universe $V^{\mathcal{S}}$ over $\mathcal{S}$ is defined inductively as follows: $a\in V^{\mathcal{S}}$ if and only if $a$ is a function from $\operatorname{dom}a\subseteq V^{\mathcal{S}}$ to $\operatorname{Low}(\mathcal{S})_{\jmath}$. For each set $x$, we have the canonical representation $\check{x}$ of $x$ defined by $\operatorname{dom}\check{x}=\{\check{y}\mid y\in x\}$ and $\check{x}(\check{y})=\top$. Then define the Heyting interpretation $[\mkern-2.0mu[\phi]\mkern-2.0mu]$ with parameters of $V^{\mathcal{S}}$ as follows:

• •

  $[\mkern-2.0mu[a=b]\mkern-2.0mu]=\left(\bigwedge_{x\in\operatorname{dom}a}a(x)\to\bigvee_{y\in\operatorname{dom}b}b(y)\land[\mkern-2.0mu[x=y]\mkern-2.0mu]\right)\land\left(\bigwedge_{y\in\operatorname{dom}b}b(y)\to\bigvee_{x\in\operatorname{dom}a}a(x)\land[\mkern-2.0mu[x=y]\mkern-2.0mu]\right)$,

• •

  $[\mkern-2.0mu[a\in b]\mkern-2.0mu]=\bigvee_{y\in\operatorname{dom}b}b(y)\land[\mkern-2.0mu[a=y]\mkern-2.0mu]$,

• •

  $[\mkern-2.0mu[\bot]\mkern-2.0mu]=\bot$, $[\mkern-2.0mu[\phi\land\psi]\mkern-2.0mu]=[\mkern-2.0mu[\phi]\mkern-2.0mu]\land[\mkern-2.0mu[\psi]\mkern-2.0mu]$, $[\mkern-2.0mu[\phi\lor\psi]\mkern-2.0mu]=[\mkern-2.0mu[\phi]\mkern-2.0mu]\lor[\mkern-2.0mu[\psi]\mkern-2.0mu]$, and $[\mkern-2.0mu[\phi\to\psi]\mkern-2.0mu]=[\mkern-2.0mu[\phi]\mkern-2.0mu]\to[\mkern-2.0mu[\psi]\mkern-2.0mu]$,

• •

  $[\mkern-2.0mu[\forall x\in a\phi(x)]\mkern-2.0mu]=\bigwedge_{x\in\operatorname{dom}a}a(x)\to[\mkern-2.0mu[\phi(x)]\mkern-2.0mu]$ and $[\mkern-2.0mu[\exists x\in a\phi(x)]\mkern-2.0mu]=\bigvee_{x\in\operatorname{dom}a}a(x)\land[\mkern-2.0mu[\phi(x)]\mkern-2.0mu]$,

• •

  $[\mkern-2.0mu[\forall x\phi(x)]\mkern-2.0mu]=\bigwedge_{x\in V^{\mathcal{S}}}[\mkern-2.0mu[\phi(x)]\mkern-2.0mu]$ and $[\mkern-2.0mu[\exists x\phi(x)]\mkern-2.0mu]=\bigvee_{x\in V^{\mathcal{S}}}[\mkern-2.0mu[\phi(x)]\mkern-2.0mu]$.

Then the interpretation validates every axiom of $\mathsf{CZF^{-}}$ and more:

Let us finish this subsection with some constructors, which we need in a later proof.

$\mathsf{up}(a,b)$ represents the unordeded pair $\{a,b\}$ over $V^{\mathcal{S}}$. Hence the name $\mathsf{op}(a,b)$ represents the ordered pair given by $a$ and $b$ over $V^{\mathcal{S}}$.

Our main tool in this paper is the Heyting-valued interpretation with the double negation formal topology. Unlike set-sized realizability or set-represented formal topology, the double negation topology and the resulting Heyting-valued interpretation need not be absolute between BCST-regular sets or transitive models of $\mathsf{CZF^{-}}$. Hence we need a careful analysis of the double negation formal topology, which is the aim of this subsection.

We can see that the class of lower sets $\operatorname{Low}(\Omega)$ is just the power set of 1, and the nucleus of $\mathcal{S}$ is given by the double complement

Hence the elements of $\operatorname{Low}(\Omega)_{\jmath}$ is the collection of all stable subsets of 1, that is, a set $p\subseteq 1$ such that $p=p^{\lnot\lnot}$.

We will frequently mention the relativized Heyting-valued interpretation, the definition of relativized one is not different from the usual $V^{\Omega}$ and $[\mkern-2.0mu[\cdot]\mkern-2.0mu]$, thus we do not introduce its definition. Notwithstanding that, it is still worth mentioning the notational convention for relativization:

Note that the definition of $\tilde{A}$ makes sense due to subsection 4.2. We often confuse $\tilde{A}$ and $A^{\Omega}$ if context is clear. It is also worth to mention that if $j$ is an elementary embedding, then $j(\tilde{K})=\widetilde{j(K)}$, so we may write $j^{n}(\tilde{K})$ instead of $\widetilde{j^{n}(K)}$.

We cannot expect that $\operatorname{Low}(\Omega)$ is absolute between transitive models of $\mathsf{CZF^{-}}$, and as a result, we do not know whether its Heyting-valued universe $V^{\Omega}$ and Heyting-valued interpretation $[\mkern-2.0mu[\cdot]\mkern-2.0mu]$ is absolute. Fortunately, the formula $p\in\operatorname{Low}(\Omega)_{\jmath}$ is $\Delta_{0}$, so it is absolute between transitive models of $\mathsf{CZF^{-}}$. As a result, we have the following absoluteness result on the Heyting-valued universe:

We extended nucleus $\jmath$ to $J$ for subclasses of $\operatorname{Low}\mathcal{S}$, and use it to define the validity of formulas of the forcing language. We are working with the specific formal topology $\mathcal{S}=\Omega$, and in that case, $JP$ for a class $P\subseteq 1$ coincides with $JP=\bigcup\{q^{\lnot\lnot}\mid q\subseteq P\}$. It is easy to see that $P\subseteq JP\subseteq P^{\lnot\lnot}$. We also define the following relativized notion for any transitive class $A$ such that $1\in A$:

If $P\in A$, then $J^{A}P=P^{\lnot\lnot}$, and in general, we have $P\subseteq J^{A}P\subseteq JP\subseteq P^{\lnot\lnot}$. Moreover, we have

However, the following proposition shows that we cannot prove they are the same from $\mathsf{CZF^{-}}$:

$J^{A}$ has a crucial role in defining Heyting-valued interpretation, but it could differ from transitive set to transitive set. It causes absoluteness problems, which is apparently impossible to emend in general. The following lemma states facts on relativized Heyting interpretations:

As a final remark, note that we may understand the forcing over $\Omega$ as a double negation translation à la forcing. See 2.3 of [11] or [6] for details.