Proof. Clearly, Powerset implies the above claim. Conversely, for given set \(a\), consider \(c=\{\operatorname{ran}f \mid f\colon a\to a\times 2\}\). Then we have \[\{g\in c \mid \forall x\in a\exists i\in 2 (\langle x,i\rangle\in g)\}\] is the set of all functions from \(a\) to \(2\). Hence, Powerset holds. ◻

Proof. For notational convenience, let us omit superscripts from \(\mathcal{A}^{A,B}\) and write \(\mathcal{A}\). We can see that \(\mathcal{A}(R)\colon A\rightrightarrows S\) is equivalent to \[\forall a\in A \exists s\in S \bigl(\langle a,s\rangle \in \mathcal{A}(R)\bigr).\] We can see that this is equivalent to \[\label{Formula:Mvaluedftn95eq00} \forall a\in A \exists s\in S [\exists b\in B (s=\langle a,b\rangle \land \langle a,b\rangle\in R)].\tag{1}\] by the definition of \(\mathcal{A}\). Hence the above statement is equivalent to \(\forall a\in A\exists b\in B[ \langle a,b\rangle\in R\cap S]\), which means \(R\cap S\colon A\rightrightarrows B\). The proof of the second statement is similar: \(\mathcal{A}(R)\colon A\leftleftarrows S\) is equivalent to \[\forall s\in S \exists a\in A [\langle a,s\rangle \in \mathcal{A}(R)].\] and by unpacking \(\mathcal{A}\), we can see that the previous formula is equivalent to \[\forall s\in S \exists a\in A \bigl[\exists b\in B \bigl(s=\langle a,b\rangle \land \langle a,s\rangle\in \mathcal{A}(R)\bigr)\bigr],\] which is readily equivalent to \[\forall s\in S \exists a\in A\exists b\in B \bigl[ s =\langle a,b\rangle \in R\bigr],\] which is equivalent to \(S\subseteq R\) since \(R\subseteq A\times B\). ◻

Proof of 1. For the forward direction, let us apply the Subset Collection to \(R_u=u\). For the other direction, let \(R_u\colon a\rightrightarrows b\) be a class multi-valued function with a parameter \(u\). Here we can assume without loss of generality that \(R_u\subseteq a\times b\).

Then \(\mathcal{A}^{a,b}(R_u)\colon a\rightrightarrows a\times b\). Now apply Strong Collection to \(\mathcal{A}^{a,b}(R_u)\) to get a subimage \(r\) of \(\mathcal{A}^{a,b}(R_u)\). Hence by 2, we have that \(r\subseteq R_u\) and \(r\colon a\rightrightarrows b\). Thus, if \(c\) is full in subimages of multi-valued functions from \(a\) to \(b\), and \(d\in c\) is a subimage of \(r\), then we can see that \(d\) is also a subimage of \(R_u\). Thus \(c\) witnesses Subset Collection for \(R_u\). ◻

Proof.

1. Let \(A\) and \(B\) be sets. Apply Subset collection to \(A\), \(A\times B\) and \(R_u= \mathcal{A}(u)\). Then we can find \(\mathcal{C}\) such that \[\forall R (\mathcal{A}(R)\colon A\rightrightarrows A\times B)\implies \exists S\in \mathcal{C} (\mathcal{A}(R)\colon A\mathrel{\mathrlap{\leftleftarrows}{\rightrightarrows}}S).\] 2 implies \(\mathcal{A}(R)\colon A\rightrightarrows A\times B\) is equivalent to \(R\colon A\rightrightarrows B\), and \(\mathcal{A}(R)\colon A\mathrel{\mathrlap{\leftleftarrows}{\rightrightarrows}}S\) is equivalent to \(S\subseteq R \land R\cap S\colon A\rightrightarrows B\). By 2, we have \[\forall R (R\colon A\rightrightarrows B) \implies \exists S\in \mathcal{C} (S\subseteq R \land S\colon A\rightrightarrows B),\] Therefore, \(\mathcal{C}\) witnesses Fullness.

2. Take \(\mathcal{C}\) which is full in \(\operatorname{mv}(A,B)\). Let \(\langle R_u \mid u\in V\rangle\) be a class family and \(R_u\colon A\rightrightarrows B\). Then \(\mathcal{A}(R_u)\colon A\rightrightarrows A\times B\). By Strong Collection (see (2.2.15) of [17]), there is \(S\) such that \(A(\mathcal{R}_u)\colon A\mathrel{\mathrlap{\leftleftarrows}{\rightrightarrows}}S\), which is equivalent to \(S\subseteq R_u\) and \(S\colon A\rightrightarrows B\).

   Since \(\mathcal{C}\) is full in \(\operatorname{mv}(A,B)\), there is \(S'\in\mathcal{C}\) such that \(S'\subseteq S\) and \(S'\colon A\rightrightarrows B\). From \(S'\subseteq R_u\) and \(S'\colon A\rightrightarrows B\), we can conclude \(R_u\colon A\rightrightarrows \operatorname{ran}S'\) and \(R_u\colon \operatorname{ran}S'\rightrightarrows A\). Therefore, the set \(\{\operatorname{ran}S \mid S\in\mathcal{C}\}\) witnesses Subset Collection.

 ◻

Proof. The main idea of the proof is the same regardless of \(F\). We can see that if \(F(a)\) is a \(\Delta_0\)-subclass of a set, then we can define \(F(a)\) by using \(\Delta_0\)-Separation. Therefore, it suffices to prove \[F(a)\subseteq \{f^{-1}\{1\}\mid f:a\to F(1)\}\] because the right-hand side is a set by Replacement and Exponentiation.

For each \(b\in F(a)\), consider its characteristic function \(\chi_b:a\to\mathcal{P}(1)\) defined by \(\chi_b(x) = \{0\mid x\in b\}\). We can see that \(b=\chi_b^{-1}\{1\}\). It remains to show that \(\operatorname{ran}\chi_b \subseteq F(1)\), which will ensure \(\chi_b\) is a function of codomain \(F(1)\). Its proof depends on \(F\), but all proofs employ the following equivalence:

\[\label{Formula:CharFtnEquivalence} x\in b\iff 0\in \chi_b(x).\tag{3}\] Let us examine its proof case by case.

1. Case \(F=\mathcal{P}\): Obvious.

2. Case \(F=\mathcal{P}^{\lnot\lnot}\): Let \(b\in \mathcal{P}^{\lnot\lnot}(a)\). Then we have \(\lnot\lnot(x\in b)\to x\in b\) for all \(x\in a\), and this is equivalent to \[\lnot\lnot(0\in \chi_b(x))\to 0\in \chi_b(x)\] by 3 . Hence \(\chi_b(x)\in \mathcal{P}^{\lnot\lnot}(1)\).

3. Case \(F=\operatorname{WDec}\): Similarly, we will show \(\operatorname{ran}\chi_b \subseteq \operatorname{WDec}(1)\) if \(b\in \operatorname{WDec}(a)\). By the assumption on \(b\), we have \[\lnot(x\in b) \lor \lnot\lnot(x\in b),\] for all \(x\in a\), which turns out to be equivalent to \[\lnot(0\in \chi_b(x)) \lor \lnot\lnot(0\in \chi_b(x))\] by 3 . Therefore, \(\chi_b(x) \in \operatorname{WDec}(1)\).

4. Case \(F=\operatorname{Dec}\): Similar to the case \(\operatorname{WDec}\), so we omit it.

 ◻

Proof. Let \(\prec\) be a \(\Delta_0\)-definable relation which is extensional and satisfies the \(\prec\)-induction scheme. Then the following formula describes \(z=\operatorname{ext}_\prec(x)\): \[\exists a [\forall y\in A (y\prec x \to y\in a)] \land [\forall y\in A (y\in z\leftrightarrow y\in a\land y\prec x)]. \qedhere\] ◻

Proof. Let \(\Phi(f)\) be the following formula: \[[\text{f is a function}]\land \bigl[\forall x\in\operatorname{dom}f \bigl( \operatorname{ext}_\prec(x)\subseteq \operatorname{dom}f\bigr)\bigr] \land \bigl[\forall z\in\operatorname{dom}f \bigl( f(z) = G(f\mkern-5mu\upharpoonright\operatorname{ext}_\prec(z) )\bigr)\bigr]\] We will prove the following two lemmas before constructing the desired \(F\).

The main theorem follows by letting \(F=\bigcup\{f : \Phi(f)\}\). ◻

Proof. We only give a proof for the last statement. Let \(y\in \mathcal{P}(x)^{\lnot\lnot}\), that is, \[\lnot\lnot(\forall z: z\in y\to z\in x).\] Since we have \(\lnot\lnot\forall z\phi(z)\to \forall z[\lnot\lnot\phi(z)]\) and \(\lnot\lnot(p\to q)\to (\lnot\lnot p\to\lnot\lnot q)]\), we can derive \(\forall z\in y: \lnot\lnot(z\in x)\). That is, we have \(y\subseteq x^{\lnot\lnot}\). ◻

Proof. If \(y\in x^{\lnot\lnot}\), then \(\lnot\lnot(y=0 \land 0\in x)\) holds, which is equivalent to \[\lnot\lnot(y=0) \land \lnot\lnot(0\in x).\] Since \(y=0\) is a negation of the statement ‘\(y\) is inhabited’, \(\lnot\lnot(y=0)\) is just \((y=0)\). Therefore \(x^{\lnot\lnot}\subseteq \{0\mid \lnot\lnot(0\in x)\}\). The reverse inclusion can be shown easily. ◻

Proof. Let us remind that von Neumann hierarchies are defined by \(V_\alpha = \bigcup_{\beta<\alpha}\mathcal{P}(V_\beta)\). We claim \(V_{n+1}= \mathcal{P}(V_n)\) for a natural number \(n\) by induction on \(n\). Then the desired theorem follows from 4.

This is obvious if \(n=0\). If \(V_{k+1} = \mathcal{P}(V_k)\) for all \(k<n\), then \[\begin{array}{lll} V_{n+1} &= \bigcup_{k<n}\mathcal{P}(V_k) \cup \mathcal{P}(V_n) & \\ &= \bigcup_{k<n}V_{k+1}\cup \mathcal{P}(V_n) & (\because \text{ Inductive assumptions.})\\ &= V_n \cup \mathcal{P}(V_n) & (\because \text{ \langle V_k\mid k\in n\rangle is increasing under \subseteq.})\\ &= \mathcal{P}(V_n) & (\because \text{ V_n is transitive so V_n\subseteq\mathcal{P}(V_n).}) \end{array}\] Now the stability of \(V_n\) easily follows from 4 and induction on \(n\).

For the second assertion, if \(x\in V_\omega=\bigcup_{n\in\omega} \mathcal{P}(V_n)\), then \(x\) is a subset of some \(V_n\). By Powerset, each \(V_n\) is a set. In addition, we have \(x^{\lnot\lnot}\subseteq V_n^{\lnot\lnot}=V_n\), and thus \(x^{\lnot\lnot}\) exists by Bounded Separation. ◻

Proof. \(V_2\) is a double complement of itself, but not a subset of \(1\). ◻

Proof. We only give a proof for the former statement, as the proof of the latter statement is analogous. Since \(2\subseteq\mathcal{P}(1)\), we have \(2\subseteq \mathcal{P}(1)^{\lnot\lnot}= \mathcal{P}(1)\). It remains to show the reverse inclusion. Let \(x\subseteq 1\). We must show that \[\lnot\lnot(x=0 \lor x=1).\] But this follows from \(\lnot\lnot(0\in x\lor 0\notin x)\) and \(\lnot\lnot(x\subseteq 1)\). ◻

Proof. 3 implies \(\mathcal{P}(1)\) exists. Moreover, 3 states that the existence of \(\mathcal{P}(1)\) implies \(\mathsf{Pow}\). ◻

Proof. No \(y\) can satisfy both \(y\in x^{\lnot\lnot}\) and \(y\notin x\), which have to exist if \(x^{\lnot\lnot}\) is inexhaustible. ◻

Proof. The Axiom of Subcountability proves \(\mathcal{P}(\omega)\) is inexhaustible (See [17].) However, 7 proves \(\mathcal{P}(1)=2^{\lnot\lnot}\) is never inexhaustible. ◻

Proof.

1. One direction directly follows from 2. The other direction follows from the equiconsistency of \(\mathsf{CZF+\Delta_0\mhyphen LEM}\) and \(\mathsf{CZF+Pow}\) in [19] since \(\mathsf{\Delta_0\mhyphen LEM}\) proves every set is stable.

2. In fact, the Axiom of Subcountability proves \(\lnot\mathsf{Pow}\). In \(\mathsf{CZF}\), \(\mathsf{Pow}\) holds if and only if \(\mathcal{P}(1)\) exists. Since \(2^{\lnot\lnot}=\mathcal{P}(1)\), 2 is an instance of \(\mathsf{NDCom}\). Moreover, [20] proves \(\mathsf{CZF}\) and \(\mathsf{CZF}\) + Axiom of Subcountability are equiconsistent.

 ◻

Proof. By [21], \(\mathsf{CZF}^-\) and \(\mathsf{CZF}\) are equiconsistent. Therefore \(\mathsf{CZF^-}\) + \(\mathsf{NDCom}\) and \(\mathsf{CZF^-}\) are equiconsistent. Moreover, [22] proves \(\mathsf{CZF}^-\) and \(\mathsf{CZF}^-\) + \(\mathsf{\Delta_0\mhyphen LEM}\) are equiconsistent. From the fact that \(\mathsf{\Delta_0\mhyphen LEM}\) proves every set is stable, we have the equiconsistency between \(\mathsf{CZF}^-\) and \(\mathsf{CZF^-+DCom}\). ◻

Proof.

1. Without loss of generality, assume that there is \(t\) such that \(t\in x\) but \(t\notin y\). Define \(w_c\) by \[w_c = \{z\in x \mid 0\in c\}\cup \{z\in y \mid 0\notin c\}.\] Then \(\lnot\lnot(w_c\in a)\). Now we will prove that \(c=\{0\mid w_c=x\}\) for all \(c\subseteq 1\): one inclusion is obvious. For the reverse inclusion, let \(w_c=x\). Then \(t\in w_c\), which is equivalent to \[(t\in x\land 0\in c)\lor (t\in y\land 0\notin c).\] We can exclude the latter case as \(t\notin y\). Hence \(0\in c\) and we have \(\{0\mid w_c=x\}\subseteq c\). Therefore we have \(\mathcal{P}(1)\subseteq \{\{0\mid z=x\}\mid z\in a^{\lnot\lnot}\}\).

2. For each \(c\subseteq 1\) define \(w_c\) as before. We can deduce \(\lnot\lnot (w_c\in a)\) from \(\lnot\lnot(0\in c\lor 0\notin c)\). We claim that \(\mathcal{P}^{\lnot\lnot}(1) \subseteq \{\{0\mid z=x\}\mid z\in a^{\lnot\lnot}\}\). This would follow from \(c = \{0\mid w_c=x\}\) for stable subset \(c\) of 1. \(c\subseteq \{0\mid w_c= z\}\) is obvious. For the reverse inclusion, suppose that \(w_c=x\). Since \(x\neq y\), \(w_c\neq y\) holds so we have \(\lnot\lnot(0\in c)\). Therefore \(0\in c\) by stability of \(c\).

3. Suppose that \(x\in a\) and \(y\in x\). For each \(c\in \operatorname{WDec}(1)\), define \(w_c = (x\setminus\{y\})\cup \{y\mid 0\in c\}\). We can show that \(\operatorname{WDec}(1) \subseteq \{\{0\mid z=x\} : z\in a^{\lnot\lnot}\}\) by verifying \(c=\{0\mid w_c=x\}\) for each \(c\in \operatorname{WDec}(1)\). The proof is similar to previous cases, so we omit the details.

 ◻

Proof. [Corollary:OtherDcom1] obviously implies [Corollary:OtherDcom2]. [Corollary:OtherDcom2] implies [Corollary:OtherDcom4] by [Proposition:SomeSetsWithoutDCom]. By [19], [Corollary:OtherDcom4] and [Corollary:OtherDcom3] have the same consistency strength. Moreover, [Corollary:OtherDcom3] implies [Corollary:OtherDcom1] by 3. ◻

Proof. By 10, the absence of \(\operatorname{WDec}(1)\) implies the absence of the double complement of sets that contain an inhabited element. Hence if \(a\) has a double complement, then every element of \(a\) must be empty. That is, we have \(a\subseteq \{0\} = 1\). This is the very definition of \(\mathsf{ADCom}\).

Conversely, assume that \(\mathsf{ADCom}\) holds. Then \(\{1\}\) does not have a double complement. Therefore, \(\{x\subseteq 1 \mid \lnot\lnot(x=1)\}\) is not a set. Hence \(\operatorname{WDec}(1) = \{0\}\cup \{x\subseteq 1 \mid \lnot\lnot(x=1)\}\) is also not a set. ◻

Proof. Let \(\Phi\) be an inductive definition defined as follows: \(\langle a,x\rangle \in\Phi\) if and only if \(x\) is a function of domain \(\uparrow p\) for some \(p\in\mathbb{P}\) which satisfies the following conditions:

1. \(x(q)\subseteq a\) for every \(q\ge p\),

2. For each \(q\ge p\) and \(y\in x(q)\), \(y\) is a function of domain \(\uparrow q\) and

3. If \(p\le q\le r\) then \(y\mkern-5mu\upharpoonright(\uparrow r) \in x(r)\) for every \(y\in x(q)\).

By Class Inductive Definition Theorem, 2, there is a smallest \(\Phi\)-closed class \(I\) and a \(\Gamma_\Phi\)-hierarchy \(\langle I^\alpha \mid \alpha\in\mathrm{Ord}\rangle\). Now define

• \(V^\mathbb{P}(p) = \{x\in I\mid \operatorname{dom}x=(\uparrow p)\}\),

• \(V_\alpha^\mathbb{P}(p) = \{x\in I^\alpha\mid \operatorname{dom}x=(\uparrow p)\}\), and

• \(\tau_{pq}(x) = x\mkern-5mu\upharpoonright(\uparrow q)\) for \(x\in V^\mathbb{P}(p)\).

We will show that the conditions in 10 hold for \(V_\alpha^\mathbb{P}(p)\) and \(\tau_{pq}\). Condition [Labeling:SetKripke1], [Labeling:SetKripke2] and [Labeling:SetKripke3] are easy to check. Hence let us check the condition [Labeling:SetKripke4] holds.

Assume inductively that [Labeling:SetKripke4] holds for every \(\beta\in\alpha\). For the one direction, let \(x\in V^\mathbb{P}_\alpha(p)\), which is equivalent to \(\operatorname{dom}x=\uparrow p\) and \(x\in I^\alpha = \Gamma_\Phi(I^{\in\alpha})\). Hence, there is \(a\) such that \(a\subseteq I^{\in\alpha}\) and \(\langle a,x\rangle \in \Phi\). Condition [Labeling:DefFormulaPhi1] and [Labeling:DefFormulaPhi2] of the defining formula of \(\Phi\), combining with the inductive definition, implies \(x(q)\subseteq \bigcup_{\beta\in\alpha} V^\mathbb{P}_\beta(q)\) for every \(q\ge p\). Moreover, [Labeling:DefFormulaPhi3] is just another way to state \(\tau_{qr}''[x(q)]\subseteq x(r)\) for every \(p\le q\le r\).

For the remaining direction, assume that \(x\) is a function with the domain \(\uparrow p\) which satisfies conditions in [Labeling:SetKripke4]. We can see that the first condition implies [Labeling:DefFormulaPhi1] and [Labeling:DefFormulaPhi2]. We have observed that [Labeling:DefFormulaPhi3] is equivalent to the second condition of [Labeling:SetKripke4]. This completes the proof. ◻

Proof. Direct from the inductive definition of the universe of Kripke sets \(V^\mathbb{P}\). ◻

Proof. Direct from the definition of \(=\), \(\in\) of the Kripke language, and the monotonicity condition for Kripke sets. ◻

Proof. The proof for intuitionistic logic is similar to [26], so we omit its proof. Equality axioms directly follow from the definition of \(=\) and \(\in\), with 10. (See [9] for the list of equality axioms.) ◻

Proof.

1. Extensionality: This directly follows from the definition of \(\in\) and \(=\) of Kripke models.

2. Pairing: We will see that \(\operatorname{up}(x,y)\) witnesses Pairing for each \(x,y\in V^\mathbb{P}(p)\). We have to check the following holds: \[p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\forall z [z\in\operatorname{up}(x,y)\leftrightarrow (z=x\lor z=y)].\] In one direction, take \(q\ge p\), \(z\in V^\mathbb{P}(q)\) and suppose that \(r \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash z\in \operatorname{up}(x,y)\) holds for \(r\ge q\). Then \(\tau_{qr}(z) \in \{\tau_{pr}(x),\tau_{pr}(y)\}\), so \(\tau_{qr}(z) = \tau_{pr}(x)\) or \(\tau_{qr}(z) = \tau_{pr}(y)\). By the definition of \(\tau\), it implies

   • \(z(s) = x(s)\) for every \(s\ge r\) or

   • \(z(s) = y(s)\) for every \(s\ge r\).

   Therefore \(r \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash x=z\lor y=z\). The other direction follows from reversing our previous proof.

3. Union: We can prove that \(\operatorname{Union}(x)\) witnesses Union. The details are left to the readers.

4. \(\in\)-Induction: We have to show that \[\bot \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\forall x(\forall y\in x \phi(y)\to\phi(x)) \to \phi(x).\] Suppose that \[\label{Formula:InInductionKrikpe00} p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\forall x (\forall y\in x\phi(y)\to\phi(x))\tag{5}\] holds. We shall verify \(p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\forall x\phi(x)\), which is equivalent to \[\label{Formula:InInductionKrikpe01} \forall \beta\in\mathrm{Ord}\bigl[\forall q\ge p \forall x\in V^\mathbb{P}_\beta(q)[q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\phi(x)]\bigr].\tag{6}\] Note that the equivalence follows from the tautology \([(\exists x\phi(x)) \to \psi]\leftrightarrow [\forall x (\phi(x)\to\psi)]\) of intuitionistic logic, where \(x\) does not occur free in \(\psi\).

   Now assume inductively that 6 holds for every \(\beta\in \alpha\). Fix \(q\ge p\) and let \(x\in V^\mathbb{P}_\alpha(q)\). If \(y\in x(r)\) for \(r\ge q\), then \(y\in V^\mathbb{P}_\beta(r)\) for some \(\beta\in\alpha\). Therefore \(r \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\phi(y)\) for all \(r\ge q\) and \(y\in x(r)\). This implies \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\forall y\in x \phi(y)\). By 5 , \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\forall y\in x \phi(y)\) implies \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\phi(x)\). By induction on ordinals over the ground model \(V\), we have 6 for every \(\beta\in \mathrm{Ord}\).

5. Infinity: We shall prove that \(\check{\omega}\) witnesses Infinity. Formally, \(\check{\omega}\) is closed under successor operator \(x\mapsto x\cup\{x\}\) internally. By induction on \(n\), we can prove \[\bot \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash{\mathpalette\@widecheck{(n+1)}} = \check{n}\cup \{\check{n}\}.\] Moreover, \(\check{\omega}(p) = \{\tau_{\bot p}(\check{n}) \mid n\in\omega\}\). Therefore, if \(p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash x\in\check{\omega}\), which implies \(x=\tau_{\bot p}(\check{n})\) for some \(n\in\omega\), then we have \(p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash x\cup\{x\} \in \check{\omega}\).

6. (\(\Delta_0\)-)Separation: Let \(x,y\in V^\mathbb{P}(p)\) be Kripke names. Since our ground model satisfies \(\Delta_0\)-separation, \(\operatorname{Sep}_\phi(x;y_0,\cdots,y_n)\) is a set for a bounded formula \(\phi(x,y_0,\cdots,y_n)\). We can easily see that \[p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\forall z [z\in \operatorname{Sep}_\phi(x;y_0,\cdots, y_n) \leftrightarrow z\in x\land \phi(z,y_0,\cdots, y_n)]\] by the definition of \(\operatorname{Sep}_\phi(x;y_0,\cdots y_n)\). The same proof can be applied to show \(V^\mathbb{P}\) satisfies Full separation in the case when \(V\) satisfies Full separation.

7. Strong Collection: Fix \(p\in\mathbb{P}\) and \(a\in V^\mathbb{P}(p)\). Suppose that \(q\ge p\) satisfies \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\forall x\in a \exists y \phi(x,y)\), which is equivalent to \[\label{Formula:StrCollKripke00} \forall r\ge q\forall x\in a(r) \exists y \bigl[ y\in V^\mathbb{P}(r) \land r \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\phi(x,y)\bigr].\tag{7}\] Define \(A=\bigcup_{r\ge q}\{r\}\times a(r)\). Then 7 can be restated as \[\label{Formula:StrCollKripke01} \forall \pi \in A\exists y [y \in V^\mathbb{P}(\jmath_0\pi) \land \jmath_0\pi \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\phi(\jmath_1\pi, y)].\tag{8}\] (where \(\jmath_0\) and \(\jmath_1\) are canonical projections of a pairing.) By Strong Collection in \(V\), we can find a set \(C\) such that \[\label{Formula:StrCollKripke02} \forall \pi \in A\exists y\in C [y \in V^\mathbb{P}(\jmath_0\pi) \land \jmath_0\pi \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\phi(\jmath_1\pi, y)]\tag{9}\] and \[\label{Formula:StrCollKripke03} \forall y\in C\exists \pi \in A [y \in V^\mathbb{P}(\jmath_0\pi) \land \jmath_0\pi \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\phi(\jmath_1\pi, y)].\tag{10}\] \(C\) itself is not a \(\mathbb{P}\)-name, but a collection of \(\mathbb{P}\)-names. Now let us turn \(C\) to a \(\mathbb{P}\)-name witnessing the instance of Strong Collection. Let us define \(b\in V^\mathbb{P}(q)\) as follows: \[\label{Formula:StrCollInstanceB} b(r) = \{\tau_{sr}(y) \mid y\in C\land q\le s\le r \land \operatorname{dom}y = \uparrow s \}.\}\tag{11}\] \(b\) is well-defined by Replacement and \(\Delta_0\)-Separation. We will show that \(b\in V^\mathbb{P}(q)\) and \(b\) witnesses Strong Collection. Note that we do not need the full \(b(r)\) as an instance of a collection set. In fact, a subset \(\{y\in C \mid \operatorname{dom}y = \uparrow s\}\) suffices to witness Strong Collection. However, other \(\mathbb{P}\)-names are essential for the monotonicity of \(b\).

   We can easily show \(b\in V^\mathbb{P}(q)\) by checking conditions in 8. It remains to show that \(b\) witnesses Strong Collection. We shall prove \[q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\forall x\in a \exists y\in b \phi(x,y) \land \forall y\in b \exists x\in a \phi(x,y).\] However, this is a direct corollary of 9 , 10 and the definition of \(b\).

8. Subset Collection: We will show that \(V^\mathbb{P}\) validates Fullness if \(V\) satisfies Subset Collection. We shall prove \[\bot \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\forall a, b\exists c [\forall x\colon a\rightrightarrows b \exists y\in c [y\colon a\rightrightarrows b\land\, y\subseteq x]].\] Fix \(p\in\mathbb{P}\) and \(a,b\in V^\mathbb{P}(p)\). Notice that for \(q\ge p\) and \(x\in V^\mathbb{P}(q)\), we have \[\begin{align} q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash x\colon a\rightrightarrows b &\iff q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\forall u\in a\exists v\in b [ \operatorname{op}(u,v)\in x] \\ &\iff \forall r\ge q \forall u\in a(r) \exists v\in b(r)[ \operatorname{op}(u,v)\in x(r)]. \end{align}\] For each \(q\ge p\), let \(A_q=\bigcup_{r\ge q} \{r\}\times a(r)\) and \(B = \bigcup_{r\ge p} b(r)\). Now consider the following relation with the parameter \(x\): \[R_x = \{\langle \langle r,u\rangle, v\rangle \in A_q\times B \mid \operatorname{dom}v = \uparrow r\land \operatorname{op}(u,v) \in x(r).\}\] We can see that \(R_x\subseteq A_q\times B\) and \(R_x\colon A_q\rightrightarrows B\). Now apply Subset Collection to \(\mathcal{A}^{A_q, B}(R_x)\), where \(\mathcal{A}^{A_q, B}\) is defined in 2. Then we have a family \(\mathcal{F}\) of sets, depending on \(q\ge p\), such that \[\forall x \bigl[\bigl(\mathcal{A}^{A_q, B}(R_x)\colon A_q\rightrightarrows A_q\times B \bigr) \to \bigl(\exists C\in \mathcal{F} (\mathcal{A}^{A_q, B}(R_x) \colon A_q \mathrel{\mathrlap{\leftleftarrows}{\rightrightarrows}}C)\bigr)\bigr].\] By 2, this is equivalent to \[\label{Formula:SubCollKripke00} \forall x [ (R_x\colon A_q\rightrightarrows B) \to \exists C\in \mathcal{F} \colon C\subseteq R_x \land C\colon A_q\rightrightarrows B].\tag{12}\] In sum, we have for each \(q\ge p\) there is \(\mathcal{F}\) satisfying 12 . Then apply Collection to the previous claim to get a set \(\mathbb{C}\), which satisfies for each \(q\ge p\) there is \(\mathcal{F}\in\mathbb{C}\) such that 12 holds.

   Now let us start the construction of a \(\mathbb{P}\)-name witnessing Fullness. We first define a classification of relations given as follows: \[\label{Formula:SubCollKripke01} \mathcal{Z}_q = \{\mathcal{F}\cap \operatorname{mv}(A_q,B) \mid \mathcal{F}\in\mathbb{C}\}.\tag{13}\] Since the formula “\(R\in \operatorname{mv}(A_q,B)\)” is \(\Delta_0\), \(\mathcal{F}\cap\operatorname{mv}(A_q,B)\) is a set. Hence \(\mathcal{Z}_q\) is a set for each \(q\ge p\).

   Now for each \(C\in \mathcal{Z}_q\), define \[\label{Formula:SubCollKripke02} z_{q,C}(r) = \{ \tau_{sr}(\operatorname{op}(u,v)) \mid q\le s\le r \land \langle \langle s,u\rangle, v\rangle \in C \land \operatorname{dom}v = \uparrow s\}.\tag{14}\] \(z_{q,C}\) itself does not witness Fullness, but is an element of a name witnessing Fullness. Note that \(z_{q,C}\in V^\mathbb{P}(q)\) by 8. Now let us define a name \(c\) with domain \(\uparrow p\) as follows: \[c(q) = \{\tau_{sq}(z_{s,C}) \mid p\le s\le q \land C\in \mathcal{Z}_q\}.\] We can see that \(c\) is a name by 8.

   It remains to show that \(c\) witnesses Fullness: For given \(x\in V^\mathbb{P}(q)\) satisfying \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash x\colon a\rightrightarrows b\), we can find \(\mathcal{F}\in\mathbb{C}\) and \(C\in\mathcal{F}\) such that the consequent of 12 holds. By definition of \(z_{q,C}\) and \(C\subseteq R_x\), we have \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash z_{q,C}\subseteq x\). Since \(z_{q,C}\in c(q)\), \(c\) witnesses Fullness.

9. Powerset: Let us assume Powerset over \(V\). We can show that \(\operatorname{Power}(x)\) exists for \(x\in V^\mathbb{P}\). Moreover, we can prove that \(\operatorname{Power}(x)\) witnesses Powerset. The full proof is left to the readers, but note that the following equivalence is useful: \[p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash y\subseteq x\iff \forall q\ge p : y(q)\subseteq x(q). \qedhere\]

 ◻

Proof. \(\vartriangleleft\) has a \(\Delta_0\)-definition. Moreover, \(\operatorname{ext}_\vartriangleleft(x)=\bigcup \operatorname{ran}x\). Hence, it is sufficient to show that the \(\vartriangleleft\)-induction scheme is valid. The idea of our proof — showing the induction schema is valid by applying induction on the level of hierarchy — will be akin to that of showing \(\in\)-induction over \(V^\mathbb{P}\).

Suppose that \[\label{Formula:InductionOnTriangle} \forall x\in V^\mathbb{P}[ (\forall y\in V^\mathbb{P}: y\vartriangleleft x\to \phi(y))\to \phi(x)]\tag{15}\] holds. Furthermore, assume inductively that \(\forall x\in V^\mathbb{P}_\beta\phi(x)\) holds for all \(\beta\in\alpha\).

If \(x\in V^\mathbb{P}_\alpha\) and \(y\vartriangleleft x\), then \(y\in V^\mathbb{P}_\beta\) for some \(\beta\in\alpha\). Hence, we have \(\phi(y)\) by the inductive hypothesis. Therefore, we can derive \(\phi(x)\) from 15 . ◻

Proof. The proof uses induction on \(\vartriangleleft\). Assume that the proposition holds for all \(y\vartriangleleft x\), so we have \[\forall q\ge p\forall y\in x(q) \forall r\ge q: y(r)\subseteq V^\mathbb{P}_{\operatorname{krk}y}(r).\] By the previous sentence and the conditions on \(V^\mathbb{P}\) of [Labeling:SetKripke4], we have \(y\in V^\mathbb{P}_{\operatorname{krk}y+1}(q)\subseteq V^\mathbb{P}_{\operatorname{krk}x}(q)\) for all \(y\in x(q)\). Hence \(x(q)\subseteq V^\mathbb{P}_{\operatorname{krk}x}(q)\). ◻

Proof. \(\operatorname{krk}x\ge \operatorname{krk}\tau_{pq}(x)\) follows from that if \(y\vartriangleleft \tau_{pq}(x)\) then \(y\vartriangleleft x\). Now suppose that \(\mathbb{P}\) is linear. We will use the induction on \(\vartriangleleft\): assume that \(\operatorname{krk}y = \operatorname{krk}\tau_{pq}(y)\) holds for all \(y\vartriangleleft x\). Then \[\begin{array}{lcl} \operatorname{krk}\tau_{pq}(x) &=& \sup \{\operatorname{krk}y + 1 \mid y\vartriangleleft x\} \\ &=& \sup_{r\ge q}\sup \{\operatorname{krk}y + 1 \mid y\in x(r)\}. \end{array}\] We want to show that the last one is greater than or equal to \(\operatorname{krk}x=\sup_{r\ge p}\sup \{\operatorname{krk}y + 1 \mid y\in x(r)\}\). If \(r\ge p\), then either \(r\ge q\) or \(q\ge r\). If \(q\ge r\), then by the inductive assumption, \[\sup \{\operatorname{krk}y+1\mid y\in x(r)\} = \sup\{\operatorname{krk}\tau_{rq}(y) + 1\mid y\in x(r)\}.\] and the latter is less than or equal to \(\sup\{\operatorname{krk}y+1\mid y\in x(q)\}\) by the monotonicity of Kripke names. Thus \[\sup_{p\le r\le q}\sup\{\operatorname{krk}y+1\mid y\in x(r)\}\le \sup\{\operatorname{krk}y+1\mid y\in x(q)\}\] and we have \(\operatorname{krk}x\le \operatorname{krk}\tau_{pq}(x)\). ◻

Proof. The main idea of our proof is the same as that of showing the induction scheme for \(\vartriangleleft\). It suffices to show that the \(\in_p\)-induction schema is valid. Suppose that \[\label{Formula:InPInduction01} \forall y\in V^\mathbb{P}(p) : [y\in_p x \to \phi(y)]\to \phi(x)\tag{16}\] holds for all \(x\in V^\mathbb{P}(p)\). Now we will show that \[\label{Formula:InPInduction00} \forall \alpha\in \mathrm{Ord}\forall x\in V^\mathbb{P}_\alpha (p) : \phi(x)\tag{17}\] by induction on \(\alpha\).

Suppose that \(\forall x\in V^\mathbb{P}_\beta (p) : \phi(x)\) holds for all \(\beta\in\alpha\). If \(x\in V^\mathbb{P}_\alpha(p)\) and \(y\in x(p)\), then \(y\in V^\mathbb{P}_\beta (p)\) for some \(\beta\in\alpha\). Therefore \(\phi(y)\) holds for all \(y\in_p x\). By 16 , \(\phi(x)\) holds. Therefore \(\phi(x)\) holds for all \(x\in V^\mathbb{P}_\alpha(p)\). Hence 17 follows by the induction on ordinals. ◻

Proof. The initial three statements directly follow from the definition of \(\mathbb{s}_p\) and \(\operatorname{up}\). Hence we only give proof for the last two statements:

4. For the one inclusion, we have \[\begin{array}{lll} \mathbb{s}_p(\operatorname{Union}(x)) &= \mathbb{s}_p''[{\small\bigcup} \{z(p) \mid z\in x(p)\}] &= {\small\bigcup} \{\mathbb{s}_p''[z(p)] \mid z\in x(p)\}\\ &= {\small\bigcup}\{\mathbb{s}_p(z) \mid z\in x(p)\} &\subseteq {\small\bigcup}\mathbb{s}_p''[x(p)] \\ &= {\small\bigcup}\mathbb{s}_p(x).& \end{array}\] For the remaining inclusion, observe that \(w\in \mathbb{s}_p(x)\) if and only if \(w=\mathbb{s}_p(y)\) for some \(y\in x(p)\). Hence \(\bigcup \mathbb{s}_p(x) \subseteq \bigcup\{\mathbb{s}_p(y) \mid y\in x(p)\} = \mathbb{s}_p(\operatorname{Union}(x))\).

5. By a direct calculation, we have \[\begin{array}{ll} \mathbb{s}_p(\operatorname{Power}(x)) &= \mathbb{s}_p''[\{z\in V^\mathbb{P}(p) \mid \forall q\ge p : z(q)\subseteq x(q)\}] \\ &= \{\mathbb{s}_p(z)\mid z\in V^\mathbb{P}(p) \text{ and } \forall q\ge p : z(q)\subseteq x(q)\}\\ &\subseteq \{\mathbb{s}_p(z)\mid \mathbb{s}_p(z)\subseteq \mathbb{s}_p(x)\}\\ &\subseteq \mathcal{P}(\mathbb{s}_p(x)) \end{array}\] as \(z(p)\subseteq x(p)\) implies \(\mathbb{s}_p(z)\subseteq \mathbb{s}_p(x)\).

 ◻

Proof. Let \(\mathbb{P}\) be a linear order. \(p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\lnot\lnot(z\in x)\) implies there is \(q\ge p\) such that \(\tau_{pq}(z)\in x(q)\). Thus \(\operatorname{krk}\tau_{pq}(z)< \operatorname{krk}x\). By 12, \(\operatorname{krk}z = \operatorname{krk}\tau_{pq}(z)\), so we have the desired result. ◻

Proof of 6. Let \(x\in V^\mathbb{P}(p)\). Define a function \(y\) of domain \(\uparrow p\) as \[y(q) =\{z\in V_{\operatorname{krk}x}^\mathbb{P}(q) \mid \exists s\ge q : \tau_{qs}(z)\in x(s)\}.\] We can show \(y\in V^\mathbb{P}(p)\) by 8. We claim that \(y\) is a double complement of \(x\): that is, \[p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\forall z : \lnot\lnot (z\in x)\leftrightarrow z\in y.\] Let \(q\ge p\) and \(z\in V^\mathbb{P}(q)\). For the one direction, assume that \(r \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\lnot\lnot( z\in x)\) holds for some \(r\ge q\). By 15, we have \(\operatorname{krk}z<\operatorname{krk}x\). Thus we have \(z\in V^\mathbb{P}_{\operatorname{krk}x}(q)\) by 13 and the Closure lemma (8). Furthermore, \(r \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\lnot\lnot( z\in x)\) implies the existence of \(s\ge q\) such that \(\tau_{qs}(z)\in x(s)\). Hence \(z\in y(q)\).

For the remaining direction, let \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash z\in y\), so that \(z\in y(q)\). By definition, we have \(s\ge q\) such that \(\tau_{qs}(z)\in x(s)\). Since \(s\) is comparable with any element of \(\mathbb{P}\) due to linearity, we have \(\forall r\ge q \exists s\ge s: \tau_{qs}(z)\in x(s)\). Thus \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\lnot\lnot (z\in x)\). ◻

Proof. We are going to construct a sequence of sets of \(2^{<\omega}\)-names \(\langle C_\alpha \mid \alpha\in\mathrm{Ord}\rangle\) such that \(C_\alpha\subseteq C\) and \(|C_\alpha|=\beth_\alpha\) for every \(\alpha\). First, let us define \(C_0\subseteq C\) as the set of names \(x\in V^{2^{<\omega}}(\bot)\) satisfying the following: There is \(n<\omega\) and \(a\in V_{n+1}\setminus V_n\) such that

• \(x(p) = \varnothing\) if \(p\ngeq 0^n\), and

• \(\tau_{\bot,0^n}(x) = \tau_{\bot,0^n}(\check{a})\).

\(n\) and \(a\) uniquely specifies \(x\), and there are countably many such \(x\). Hence, \(|C_0| = \omega = \beth_0\). Now say two names \(x,y\in V^{2^{<\omega}}(0^n)\) are equal near \(0^\omega\) if there is \(m\ge n\) such that \(\tau_{\bot,0^m}(x)=\tau_{\bot,0^m}(y)\). It is clear that if \(x,y\in C_0\), then \(x=y\) iff \(x\) and \(y\) are equal near \(0^\omega\).

Now, let us assume that we are given \(C_\alpha\). We also inductively assume that for two \(x,y\in C_\alpha\), \(x=y\) iff \(x\) and \(y\) are equal near \(0^\omega\). For \(x\in V^{2^{<\omega}}(p)\), let \(f(x)\in V^{2^{<\omega}}(0^\frown p)\) be the new name recursively defined by \[f(x)(0^\frown q) = \{f(y) \mid y\in x(q)\} \text{ for }q\ge p.\] One can see that \(f(x)\) also satisfies the monotonicity condition, so \(f(x)\) is also a \(2^{<\omega}\)-name. Also, note that \(x\) and \(y\) are equal near \(0^\omega\) iff \(f(x)\) and \(f(y)\) are equal near \(0^\omega\). Given \(C_\alpha\), let us define \(C_{\alpha+1}\) to be the set of \(z\in V^{2^{<\omega}}(\bot)\) such that there is \(Z\subseteq C_\alpha\), we have

• \(z(\bot)=\varnothing\).

• \(z(1^\frown p) = \varnothing\) for every \(p\in 2^{<\omega}\).

• \(z(0^\frown p) = \bigl\{\tau_{0,0^\frown p}\bigl(f(x)\bigr) \bigm| x\in Z\bigr\}\).

We need the following lemma in a later calculation:

Now we claim that \(C_{\alpha+1}\subseteq C\): Fix \(Z\subseteq C_\alpha\) and consider the corresponding name \(z\). We want to show that \(z\in C\). To see this, we show for each \(m<\omega\) there is \(b\subseteq V_m\) such that \(\tau_{\bot,0^m 1}(z) = \tau_{\bot,0^m1}(\check{a})\). We clearly have \(\tau_{\bot,1}(z) = \tau_{\bot,1}(\check{\varnothing})\), so let us consider the case \(m=n+1\).

For each \(y\in Z\) and \(n<\omega\), let us fix \(b_y \subseteq V_n\) such that \(\tau_{\bot,0^n1}(y) = \tau_{\bot,0^n1}(\check{b}_y)\). Then we have for \(p\ge 0^n 1\), \[\begin{align} \tau_{0,0^{n+1}1}\bigl(f(y)\bigr) (0^\frown p) & = \{f(z)\mid z\in y(p)\} = \{f(z)\mid z\in \check{b}_y(p)\} \\ &= \bigl\{ f\bigl( \tau_{\bot,p}(\check{c})\bigr) \bigm| c\in b_y\bigr\} = \{\tau_{\bot,0^\frown p}(\check{c}) \mid c\in b_y\} \\ &= \check{b}_y(0^\frown p), \end{align}\] so we have \(\tau_{0,0^{n+1}1}\bigl(f(y)\bigr) = \tau_{\bot,0^{n+1}1}(\check{b}_y)\). This implies for \(p\ge 0^n 1\), \(\tau_{0,0^\frown p}\bigl(f(y)\bigr) = \tau_{\bot,0^\frown p}(\check{b}_y)\).

If we take \(a = \{b_y\mid y\in Z\}\), then \(a\subseteq V_{n+1}\) and for \(p\ge 0^n1\), \[z(0^\frown p) = \bigl\{ \tau_{0,0^\frown p}\bigl(f(y)\bigr) \bigm| y\in Z\bigr\} = \bigl\{ \tau_{\bot,0^\frown p}(\check{b}_y) \bigm| y\in Z\bigr\} = \check{a}(0^\frown p).\] This shows \(\tau_{\bot,0^{n+1}1}(z) = \tau_{\bot,0^{n+1}1}(\check{a})\), as desired.

Now we claim that if \(z_0,z_1\in C_{\alpha+1}\) are different names, then \(z_0\) and \(z_1\) are different near \(0^\omega\). Let \(Z_0,Z_1\subseteq C_\alpha\) be the subsets corresponding to \(z_0\) an \(z_1\) respectively. Without loss of generality, let us assume that there is \(x\in Z_1\setminus Z_0\). Since \(x\) is not equal to any element of \(Z_0\) near \(0^\omega\), we have \(z_0(0^n)\neq z_1(0^n)\) for all \(n<\omega\), which implies the desired result. Clearly, \(|C_{\alpha+1}| = 2^{|C_\alpha|} =\beth_{\alpha+1}\).

For a limit \(\alpha\), we take \(C_\alpha = \bigcup_{\beta<\alpha} C_\beta\). Then \(C_\alpha\subseteq C\) and two distinct names of \(C_\alpha\) are not equal near \(0^\omega\). Again, we have \(|C_\alpha| = \beth_\alpha\) for a limit \(\alpha\). ◻

Proof. If \(0^n \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\exists x \forall y [y\in x\leftrightarrow \lnot\lnot (y\in \check{V}_\omega)]\), then we can find \(x\in V^{2^{<\omega}}(0^n)\) such that for every \(p\ge 0^n\) and \(y\in V^{2^{<\omega}}(p)\) such that \(p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\lnot\lnot (y\in \check{V}_\omega)\), we have \(y\in x(p)\). However, we know that \(p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\lnot\lnot(y\in\check{V}_\omega)\) for every \(y\in C\), so \(C\subseteq x(p)\). This is impossible since \(C\) is a proper class. ◻

Proof. Suppose that \(x(q)\subseteq K^m(q)\) for all \(q\ge p\). Take \(a=\bigcup_{q\ge p} x(q)\). Then we can see that \(\langle a, x\rangle \in \Phi_m\). Since \(a\subseteq K^m\), we have \(x\in K^m(p)\). ◻

Proof. The first and second statements follow from the definition of \(K(p)\). For the third statement, observe that \(\tau_{pq}\) is just a restriction, so it does not change anything except for the domain of an input. We can show the last statement by applying set induction on \(a\): Suppose that \(\check{b}\in K^0(0)\) for all \(b\in a\). Clearly, \(\check{a}\) stops expanding hereditarily after stage 0. Hence, 16 guarantees \(\check{a}\in K^0(0)\). ◻

Proof. Let us decompose the sentence \(x(q)\subseteq \bigcup_{\beta\in\alpha} K^m_\alpha(q)\) into a conjunction of \(x(q)\subseteq \bigcup_{\beta\in\alpha} V_\alpha(q)\) and \(x(q)\subseteq K^m(q)\). Then the equivalence follows from 16 and Condition [Labeling:SetKripke4] of 10. ◻

Proof.

1. In fact, \(\mathbb{t}_s:V^\omega\to V^\omega(\ge s)\) and \(\mathbb{t}_{-s}:V^\omega(\ge s)\to V^\omega\) are inverses of each other. It can be shown by induction on \(\vartriangleleft\).

   We will show that \(\mathbb{t}_{-s} \circ \mathbb{t}_s\) is the identity map. The other equality can be shown analogously. Assume inductively that \(\mathbb{t}_{-s} \circ \mathbb{t}_s (y) = y\) holds for all \(y\vartriangleleft x\). For \(q\ge p\) and \(x\in V^\omega(p)\), we have \[\mathbb{t}_{-s}\circ \mathbb{t}_s(x)(q) = \mathbb{t}_{-s}''[\mathbb{t}_s(x)(q+s)] = \mathbb{t}_{-s}''[\mathbb{t}_s'' [(x(q)]] = x(q)\] since \(y\vartriangleleft x\) for all \(y\in x(q)\). Hence \(\mathbb{t}_{-s}\circ \mathbb{t}_s(x) = x\) for all \(x\in V^\omega\). Moreover, by examining the domains of Kripke sets, we can see that the restrictions \(\mathbb{t}_s\mkern-5mu\upharpoonright V^\omega(p)\) and \(\mathbb{t}_{-s}\mkern-5mu\upharpoonright V^\omega(p+s)\) are inverses of each other.

2. Let \(z\in \mathbb{t}_s(\tau_{pq}(x))(r+s)\) for \(p\le q\le r\), so there is \(w\in \tau_{pq}(x)(r) = x(r)\) such that \(z=\mathbb{t}_s(w)\). Hence \(z\in \mathbb{t}_s''[x(r)] = \mathbb{t}_s(x)(r+s) = \tau_{p+s,q+s}(\mathbb{t}_s(x))(r+s)\). This shows \(\mathbb{t}_s(\tau_{pq}(x))(r+s)\subseteq \tau_{p+s,q+s}(\mathbb{t}_s(x))(r+s)\). Showing the reverse inclusion is analogous, so we omit it.

3. If \(x\in K^m(p)\), then \(x(q)=\tau_{mq}''[x(p)]\) for every \(q\ge m\). We can show \(\mathbb{t}_s(x)(q+s) = \tau_{m+s,q+s}''[\mathbb{t}_s(x)(m+s)]\) for \(q\ge m\), so \(\mathbb{t}_s(x)\in K^{m+s}(p+s)\).

4. We can show the following facts. The proof is similar to what we have already done, so we omit it.

   1. \(\mathbb{t}_{-s}(\tau_{p+s,q+s}(x)) = \tau_{p,q}(\mathbb{t}_{-s}(x))\) for all \(x\in V^\omega(p+s)\) and \(p\le q\).

   2. If \(x\in K^{m+s}(p+s)\) for \(m\ge p\), then \(\mathbb{t}_{-s}(x)\in K^m(p)\).

   Therefore, \(\mathbb{t}_s: K(p)\to K(p+s)\) and \(\mathbb{t}_{-s}: K(p+s)\to K(p)\). Since the composition of the two functions is the identity, they are inverses of each other.

 ◻

Proof. By the proof of 3 of 19, we have \(\mathbb{t}_s(x)(q+s)=\tau_{p+s,q+s}''[\mathbb{t}_s(x)(p+s)]\) for \(q\ge p\). Therefore, we can see that \(\mathbb{t}_s(x)=\tau_{p,p+s}(x)\) is equivalent to \(\mathbb{t}_s(x)(p+s)=x(p+s)\) for \(x\in K^p(p)\).

We will show that \(\mathbb{t}_s(x)(p+s)=x(p+s)\) by induction: Suppose that \(x\in K^p_\alpha(p)\) and the equality holds for every \(y\in K^p_\beta(p)\) and \(\beta\in\alpha\). We have \(\mathbb{t}_s(y)=\tau_{p,p+s}(y)\) for every \(y\in x(p)\). Therefore, \(\mathbb{t}_s(x)(p+s) = \mathbb{t}_s''[x(p)] = \tau_{p,p+s}''[x(p)] = x(p+s)\). ◻

Proof. We will prove them simultaneously by induction on \(\phi\), uniform to \(p\), \(s\) and \(\vec{a}\). We will only consider \(\mathbb{t}_{+s}\), as the case for \(\mathbb{t}_{-s}\) is similar.

1. Atomic formulas: Suppose that \(p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K a_0=a_1\), which is equivalent to \(a_0=a_1\). Since \(\mathbb{t}_{\pm s}\) are one-to-one, this is equivalent to \(\mathbb{t}_s(a_0)=\mathbb{t}_{s}(a_1)\), so we have \(p+ s \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \mathbb{t}_s(a_0) = \mathbb{t}_s(a_1)\).

   If \(p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_Ka_0\in a_1\), so \(a_0\in a_1(p)\), then \(\mathbb{t}_s(a_0)\in\mathbb{t}_s''[a_1(p)] = \mathbb{t}_s(a_1)(p+s)\). Thus \(p+s \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \mathbb{t}_s(a_0)\in\mathbb{t}_s(a_1)\).

2. Binary connections: Cases for \(\land\) and \(\lor\) are easy to prove, so we omit them. We will concentrate on the case \(\to\).

   Suppose that \(p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K (\phi\to \psi)(\vec{a})\) holds: That is, for every \(q\ge p\), \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(\tau_{pq}(\vec{a}))\) implies \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \psi(\tau_{pq}(\vec{a}))\). Furthermore, let \(q+s \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(\tau_{p+s,q+s}(\mathbb{t}_s(\vec{a})))\) holds for every \(q\ge p\), which is equivalent to \(q+s \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(\mathbb{t}_s(\tau_{p,q}(\vec{a})))\). By the inductive hypothesis on \(\phi\), we have \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(\mathbb{t}_{-s}(\mathbb{t}_s(\tau_{p,q}(\vec{a}))))\), so \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K\phi(\tau_{p,q}(\vec{a}))\). Therefore, \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \psi(\tau_{pq}(\vec{a}))\) and we have \(q+s \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \psi(\mathbb{t}_s(\tau_{pq}(\vec{a}))\) by the inductive hypothesis on \(\psi\).

   In sum, \(q+s \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(\tau_{p+s,q+s}(\mathbb{t}_s(\vec{a})))\) implies \(q+s \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \psi(\tau_{p+s,q+s}(\mathbb{t}_s(\vec{a})))\) for all \(q\ge p\), which means \(p+s \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash(\phi\to\psi)(\mathbb{t}_s(\vec{a}))\).

3. Quantifiers: The case for \(\exists\) is easy to check. For the case for \(\forall\), suppose that \(p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \forall x\phi(x,\vec{a})\), which is equivalent to \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(x,\tau_{pq}(\vec{a}))\) for every \(q\ge p\) and \(x\in K(q)\). Therefore, we have \(q+s \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(\mathbb{t}_s(x),\mathbb{t}_s(\tau_{pq}(\vec{a}))\) for every \(x\in K(q)\). Since \(\mathbb{t}_s\) is an onto function from \(K(q)\) to \(K(q+s)\), we have \(q+s \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(y,\tau_{p+s,q+s}(\mathbb{t}_s(\vec{a})))\) for every \(y\in K(q+s)\). Since \(q\ge p\) is arbitrary, we have \(p+s \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K\forall x \phi(x,\mathbb{t}_s(\vec{a}))\).

 ◻

Proof. We can show Extensionality directly. For \(\in\)-induction, we can use the argument which is described in the proof of \(\in\)-induction in 5, with 18.

The main idea of a proof for Pairing, Union, and Separation is the same: we shall prove that \(K(p)\) is closed under operations \(\operatorname{Union}\), \(\operatorname{up}\) and \(\operatorname{Sep}\). For \(\operatorname{up}\), suppose that we have \(x,y\in K(p)\). Without loss of generality, we can assume that there is \(m\ge p\) such that \(x,y\in K^m(p)\). We claim that \(\operatorname{up}(x,y)\in K^m(p)\) by applying 16: it is obvious that \(\operatorname{up}(x,y)(q)\subseteq K^m(q)\) for all \(q\ge p\). Moreover, if \(q\ge m\) then \[\operatorname{up}(x,y)(q)=\tau_{pq}''\{x,y\}=\tau_{mq}''\{\tau_{pm}(x),\tau_{pm}(y)\} =\tau_{mq}''[\operatorname{up}(x,y)(m)].\] Therefore, \(\operatorname{up}(x,y)\) stops expanding hereditarily after stage \(m\). The case for \(\operatorname{Union}\) is similar, so we omit it.

For \(\operatorname{Sep}\), it is obvious that \(\operatorname{Sep}(x;\vec{y})\subseteq K^m(p)\) if \(x,\vec{y}\in K^m(p)\). Without loss of generality, assume that \(m\ge p\). To show \(\operatorname{Sep}(x;\vec{y})\) stops expanding after stage \(m\), we must check that \(\operatorname{Sep}(x;\vec{y})(q)\subseteq\tau''_{mq}[\operatorname{Sep}(x;\vec{y})(m)]\) for every \(q\ge m\).

Let \(z\in \operatorname{Sep}(x;\vec{y})(q)\). Then \(z\in x(q)\) and \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(z,\tau_{pq}(\vec{y}))\). For notational convenience, let \(s=q-m\). Since \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(z,\tau_{pq}(\vec{y}))\), we have \(m \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(\mathbb{t}_{-s}(z),\mathbb{t}_{-s}(\tau_{pq}(\vec{y}))\). Observe that \(\tau_{pm}(\vec{y})\in K^m(m)\), so we can apply 20 and we have \[\mathbb{t}_{-s}(\tau_{pq}(\vec{y})) = \mathbb{t}_{-s}(\tau_{mq}(\tau_{pm}(\vec{y}))) = \mathbb{t}_{-s}(\mathbb{t}_{s}(\tau_{pm}(\vec{y}))) = \tau_{pm}(\vec{y}).\] Therefore, \(m \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(\mathbb{t}_{-s}(z),\tau_{pm}(\vec{y}))\). Moreover, \(\mathbb{t}_s(\mathbb{t}_{-s}(z)) = z \in x(q) = \tau_{mq}''[x(m)] = \mathbb{t}_s''[x(m)]\). By injectivity of \(\mathbb{t}_s\), we can conclude \(\mathbb{t}_{-s}(z)\in x(m)\). Hence, we can conclude \(\mathbb{t}_{-s}(z)\in \operatorname{Sep}(x;\vec{y})(m)\). Since \(z\in x(q)\subseteq K^m(q) = K^q(q)\), \(z \in \tau''_{mq}[\operatorname{Sep}(x;\vec{y})(m)]\). Note that our proof works not only for Bounded separation but also for Full separation if our background theory has Full separation.

For Strong Collection and Subset Collection, we analyze the proof of 5 and modify it. For Strong Collection, let \(\phi(x,y)\) be a formula whose parameters belong to \(K(p)\). Let \(a\in K(p)\) and \(q\ge p\) satisfies \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \forall x\in a\exists y\phi(x,y)\). Take \(m>q\) large enough so that \(a\) and parameters of \(\phi\) belong to \(K^m(p)\). By the assumption on \(\phi\), we have \[\forall r\ge q\forall x\in a(r) \exists y [y\in K(r) \land r \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(x,y)].\] By letting \(A=\bigcup_{q\le r\le m}\{r\}\times a(r)\), we have the following analogue of 8 : \[\forall\pi\in A\exists y [y\in K(\jmath_0 \pi)\land \jmath_0\pi \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(\jmath_1\pi,y)].\] By Strong Collection, we can find \(C\) satisfying the following statements, which are analogues of 9 and 10 :

\[\forall \pi \in A\exists y\in C [y \in K(\jmath_0\pi) \land \jmath_0\pi \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(\jmath_1\pi, y)], \text{ and}\] \[\forall y\in C\exists \pi \in A [y \in K(\jmath_0\pi) \land \jmath_0\pi \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(\jmath_1\pi, y)].\]

We will define \(b\in K(q)\) as we define \(b\) in 11 for \(r\le m\). For \(r>m\), take \(b(r) := \tau_{mr}''[b(m)]\). That is, \(b\) is defined as follows: \[b(r) = \begin{cases} \{\tau_{sr}(y)\mid y\in C\land q\le s\le r\land \operatorname{dom}y=\uparrow s\} & \text{if r\le m},\\ \tau_{mr}'' [b(m)] & \text{if r>m}. \end{cases}\]

We claim that \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\forall x\in a\exists y\in b \phi(x,y)\). Let \(x\in a(r)\) for \(r\ge q\). If \(r\le m\), then the proof in 5 works. Now assume that \(r>m\). Then \(x=\tau_{mr}(x_0)\) for some \(x_0\in a(m)\). Hence there is \(y_0\in b(m)\) such that \(m \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(x_0,y_0)\). Therefore, \(r \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi(x,\tau_{mr}(y_0))\). This proves our desired result as \(\tau_{mr}(y_0)\in b(r)\).

It remains to show that the Axiom of Subset Collection is valid in \(K\). Since Subset Collection is equivalent to Fullness under Strong Collection, it is sufficient to check that Fullness is valid in \(K\).

Let \(a,b\in K(p)\). Take a large \(m\ge p\) satisfying \(a,b\in K^m(p)\), and follow the proof of 5 with some necessary modifications. Then define \(A_q\) and \(B\) as follows: \[A_q=\bigcup_{q\le r\le m}\{r\}\times a(r) \quad\text{ and }\quad B=\bigcup_{p\le r\le m}b(r).\] By Collection, we can find \(\mathbb{C}\) such that for each \(q\) satisfying \(p\le q\le m\), there is \(\mathcal{F}\in\mathbb{C}\) which satisfies 12 . For each \(p\le q\le m\), define \(\mathcal{Z}_q\) as in 13 . For given \(p\le q\le m\) and \(C\in\mathcal{Z}_q\), define \(z_{q,C}(r)\) same as 14 if \(q\le r\le m\). For \(r>m\), define \(z_{q,C}(r)=\tau''_{mr}[z_{q,C}(m)]\). Then we can see that \(z_{q,C}\in K^m(q)\). We finally let \[c(q)=\begin{cases} \{\tau_{sq}(z_{s,C})\mid p\le s\le q\land C\in\mathcal{Z}_q\} & \text{if q\le m,} \\ \tau_{mq}''[c(m)] & \text{if q>m.} \end{cases}\]

We claim that \(c\) witnesses Fullness. We will show that \[p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \forall x\colon a\rightrightarrows b \exists y\in c [ (y\colon a\rightrightarrows b)\land y\subseteq x].\]

Let \(q\ge p\), \(x\in K(q)\) and \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K x\colon a\rightrightarrows b\). Observe that \(a\) and \(b\) are not expanding after the stage \(m\). Consider \(x'\) of domain \(\uparrow q\) given by \[x'(r) = \begin{cases} x(r) & \text{if r\le m}, \\ \tau_{mr}''[x(m)] & \text{if r>m.} \end{cases}\] We will see that \(x'\) is a ‘support’ of \(x\) that does not expand hereditarily after stage \(m\).

By definition, \(x'\) does not grow hereditarily after stage \(m\). Furthermore, every elements of \(x\) is not expanding hereditarily after stage \(m\) as \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash x\subseteq a\times b\), and so do elements of \(x'\). Therefore, \(x'\in K^m(q)\). Moreover, it is easy to see that \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K x'\subseteq x\). Before considering \(x'\) instead of \(x\), we need to see that \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K x'\colon a\rightrightarrows b\) holds. We shall prove the following sentence: \[q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \forall u\in a\exists v\in b (\operatorname{op}(u,v)\in x').\] Let \(r\ge q\) and \(u\in a(r)\). If \(r\le m\), then this follows from \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K x\colon a\rightrightarrows b\). If \(r>m\), then \(u=\tau_{mr}(u_0)\) for some \(u_0\in a(m)\), and we can find \(v_0\in b(m)\) such that \(\operatorname{op}(u_0,v_0)\in x(m)\). Therefore, \(\operatorname{op}(u,\tau_{mr}(v_0)) = \tau_{mr}(\operatorname{op}(u_0,v_0))\in \tau_{mp}''[x(m)]=x'(r)\).

Hence, there is \(\mathcal{F}\in\mathbb{C}\) and \(C\in\mathcal{F}\) satisfying 12 for \(x'\). It remains to show that \(q \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash z_{q,C}\subseteq x'\), but this follows from \(C\subseteq R_x\) and the fact that both \(z_{q,C}\) and \(x'\) do not grow after stage \(m\). ◻

Proof. Consider the following name: \[\check{1}_p(q) = \begin{cases} \varnothing & \text{if p<q}\\ \{\check{0}\} & \text{if p\ge q}. \end{cases}\] We can see that \(\check{1}_p\in K^p(0)\) and \(0 \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \lnot\lnot(\check{1}_p=\check{1})\) holds. We prove the latter one: \(0 \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \check{1}_p\subseteq\check{1}\) is obvious. For the double negation of the remaining inclusion, observe that \(0 \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \lnot\lnot\phi\) if and only if there is \(p\) such that \(p \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash_K \phi\) due to linearity of the Kripke frame. Thus \(K\) thinks the double complement of \(\{1\}\) contains all of \(\check{1}_p\) for all \(p\in\omega\), if it exists.

However, if a Kripke set contains all of \(\check{1}_p\), then it is a subset of none of \(K^m\) for all \(m\in\omega\). Hence no Kripke sets contain all of \(\check{1}_p\). Therefore, no Kripke name is a double complement of \(\{1\}\). This proves \(\operatorname{WDec}(1)\) does not exist, and so \(\mathsf{ADCom}\) holds by 4. ◻

Proof. Let \(x\) be an \(\mathcal{A}\)-name. By 22, we can find an ordinal \(\alpha\) such that \[\forall z\in V(\mathcal{A}): V(\mathcal{A})\models z\in x \implies z\in V(\mathcal{A})_\alpha.\] Define \(y=\{\mathbf{0}\} \times V(\mathcal{A})_\alpha^{\lnot\lnot}\cap V(\mathcal{A})\). Before proceeding with the proof, we have to show that \[V(\mathcal{A})_\alpha^{\lnot\lnot}\cap V(\mathcal{A}) = \{x \in V(\mathcal{A})_\alpha^{\lnot\lnot}\mid x\in V(\mathcal{A})\}\] is a set. If \(\mathsf{\Sigma\mhyphen Sep}\) holds, then we may use the fact that \(x\in V(\mathcal{A})\) is a \(\Sigma\)-formula. We need the following fact when the case \(\mathsf{REA}\) holds: if \(B\) is a regular set, then \(B\cap V(\mathcal{A})\) is a set. (See Lemma 6.1 of [12] for its proof.) Take a regular set \(B\) that contains \(V(\mathcal{A})_\alpha^{\lnot\lnot}\). Then we have \(V(\mathcal{A})_\alpha^{\lnot\lnot}\cap V(\mathcal{A}) = V(\mathcal{A})_\alpha^{\lnot\lnot}\cap B\cap V(\mathcal{A})\), so \(V(\mathcal{A})_\alpha^{\lnot\lnot}\cap V(\mathcal{A})\) is a set. It remains to show that \[V(\mathcal{A})\models \forall z: \lnot\lnot (z\in x)\to z\in y.\] Suppose that \(e\Vdash \lnot\lnot (z\in x)\), which is equivalent to \(\lnot\lnot(\exists f\in\mathcal{A} : f\Vdash z\in x)\). Since \(\neg\neg(V(\mathcal{A})\models z\in x)\), we have \(\neg\neg (z\in V(\mathcal{A})_\alpha)\). Hence \(z\in V(\mathcal{A})_\alpha^{\lnot\lnot}\). Therefore, we can see \[\mathbf{p00} \Vdash \lnot\lnot z\in y.\] Now we can see that \(\bblambda e. \mathbf{p00}\) is a realizer of \(\mathsf{DCom}\). ◻

Proof. Let \(a\) be an instance of \(\mathsf{NDCom}\), so no set is a double complement of \(a\). Now assume that \(V(\mathcal{A})\) believes \(\check{a}\) has a double complement: formally, there is \(b\in V(\mathcal{A})\) such that \[V(\mathcal{A})\models \forall x:\lnot\lnot(x\in\check{a})\to x\in b.\] Take \(c=\{x\mid \exists e\in\mathcal{A}: e \mathrel{\text{\clipbox{0pt 0pt {.8\width} 0pt}{\Vdash}}\mkern.9mu}\vDash\check{x}\in b\}\). We will prove that \(c\) is a set by showing the following general statement: for each ordinal \(\alpha\) and a set \(x\), if \(\check{x}\in V(\mathcal{A})_\alpha\) then \(x\subseteq V_\alpha\).

Its proof uses induction on \(x\): suppose that we have \(\forall \beta\in\mathrm{Ord}[\check{y}\in V(\mathcal{A})_\beta\to y\subseteq V_\beta]\) for all \(y\in x\). Now assume that \(\check{x}=\{\langle\mathbf{0},\check{y} \rangle\mid y\in x\}\in V(\mathcal{A})_\alpha\). Then for each \(y\in x\), there is \(\beta\in \alpha\) such that \(\check{y}\in V(\mathcal{A})_\beta\). By the inductive assumption, \(y\subseteq V_\beta\) for some \(\beta\in\alpha\). Hence \(x \subseteq \bigcup_{\beta\in\alpha} \mathcal{P}(V_\beta) = V_\alpha\).

Therefore, \(c\) is equal to \(\{x\in V_\alpha \mid \exists e\in\mathcal{A} (e\Vdash \check{x}\in b)\}\) for some \(\alpha\in\mathrm{Ord}\). (Take \(\alpha\) such that \(b\in V(\mathcal{A})_\alpha\).) By 23, \(c\) is a set. Moreover, \(c\) includes a double complement of \(a\) by the following calculation: \[\begin{array}{lcl} \lnot\lnot(x\in a) &\implies& \lnot\lnot(V(\mathcal{A})\models\check{x}\in\check{a})\\ &\iff& V(\mathcal{A})\models \lnot\lnot(\check{x}\in\check{a})\\ &\implies& V(\mathcal{A})\models \check{x}\in b\\ &\implies& x\in c, \end{array}\] which contradicts the assumption that \(a\) does not have a double complement. ◻

Proof. Assume the contrary that \(\operatorname{WDec}(1)\) does not exist in \(V\), but \(V(\mathcal{A})\) thinks \(\operatorname{WDec}(1)\) exists. From \(\operatorname{WDec}(1)=\{0\}\cup \{x\subseteq 1\mid \lnot\lnot(x=1)\}\), we can deduce that the existence of \(\operatorname{WDec}(1)\) is equivalent to the existence of \(\{x\subseteq 1\mid \lnot\lnot(x=1)\}\): one direction is trivial. For the remaining direction, use \(\{x\subseteq 1\mid \lnot\lnot(x=1)\} = \operatorname{WDec}(1)\setminus\{0\}\).

Therefore, there is \(a\in V(\mathcal{A})\) and \(e\in\mathcal{A}\) such that \[\label{Formula:NotWDecPersistence00} e\Vdash\forall x: x\subseteq 1\land \lnot\lnot(x=1)\to x\in a.\tag{19}\] Now consider \(W = \{ \{0\mid \text{x is inhabited}\}\mid \exists f\in\mathcal{A}: \langle f,x\rangle\in a\}\). We claim that \(\operatorname{WDec}(1)\subseteq W\), so we have a contradiction. Let \(c\in \operatorname{WDec}(1)\). Define \[x_c = \{\langle\mathbf{0},\varnothing\rangle \mid 0\in c\}.\] We will show that \(V(\mathcal{A})\Vdash x_c\in a\). If \(c=1\), then we can see that \(\mathbf{p}(\bblambda f.\mathbf{p00})(\bblambda f.\mathbf{p00})\Vdash x_c=1\). Therefore \(\lnot\lnot (c=1)\) implies \(\lnot\lnot(\exists g: g\Vdash x_c=1)\), which is equivalent to \(\mathbf{0}\Vdash \lnot\lnot(x_c=1)\). (In fact, we can replace \(\mathbf{0}\) to any \(e\in\mathcal{A}\).) It is easy to see that \(\bblambda f.\mathbf{p00}\Vdash x_c\subseteq 1\). Combining with 19 , we have \[t\Vdash x_c\in a.\] for \(t=e\cdot \mathbf{p}(\bblambda f.\mathbf{p00})\mathbf{0}\). Hence, there is \(z\in V(\mathcal{A})\) such that \(\langle (t)_0,z\rangle\in a\) and \((t)_1\Vdash z=x_c\). We can see that \[\begin{align} 0\in c & \iff \langle \mathbf{0},\varnothing\rangle \in x_c \\ & \iff \text{z is inhabited}, \end{align}\] so \(c=\{0\mid \text{z is inhabited}\} \in W\). ◻

Proof. We start from a model \(V\) of \(\mathsf{ZFC}\) for \(T_0\), or the model constructed in [15] for \(T_1\). Let us consider the realizability models \(V(\mathcal{A})\). We know that \(V(\mathcal{A})\) satisfies \(\mathsf{IZF}\) or \(\mathsf{CZF}\) if \(V\) does. (See Chapter 3 of [11] and [12] for its proof.) Since \(V\) satisfies \(\mathsf{RDC}\) and \(\mathsf{PAx}\), \(V(\mathcal{A})\) also satisfy \(\mathsf{RDC}\) and \(\mathsf{PAx}\) by Theorem 3.1.12 of [27]. In the case of \(\mathsf{REA}\) over \(\mathsf{CZF}\), apply Theorem 6.2 of [12].

The consistency of \(T_i\) (\(i=0,1\)) with [Theorem:IZFDCom0] comes from the combination of 12, [11], ans [12] under the Kleene realizability. [Theorem:IZFDCom2] follows from 12 and [27] under \(\mathcal{A}=D_\infty\). ◻

Proof. The proof is identical to the proof of [28] except for Strong Collection. For Strong Collection, assume that we have \(e\Vdash^f \forall x\in a\exists y \phi(x,y)\). Then for each \(\langle f,x\rangle \in a\) there is \(y\in V^f(\mathcal{A})\) such that \(ef \Vdash^f \phi(x,y)\). Now choose \(y_f\) for each \(f\) by applying Global Choice. Now take \(c=\{\langle f,y_f\rangle \mid \langle f,x\rangle\in a\}\). Clearly, \(c\) is functional. Furthermore, we can see that \(c\) witnesses Strong Collection by following Swan’s proof of [28]. ◻

Proof. We proved that \(\mathsf{ZFC^- + GC}\) interprets \(\mathsf{CZF+Sep}\). Then the conclusion follows from a well-known fact that \(\mathsf{ZFC^- + GC}\) and Second-order Arithmetic are mutually interpretable. ◻

Proof. For \(X\) a subset of \(\mathcal{A}\), define \[a_X = \{\langle f,\varnothing\rangle \mid f\in X\}.\] We can see that if \(X\) is inhabited then \(\lambda f.\mathbf{p0i_r}\Vdash^f a_X\subseteq 1\). Furthermore, if \(f\in X\), then \(f\Vdash^f 0\in a_X\), and this shows \(e\Vdash^f \lnot\lnot (0\in a_X)\) for any \(e\in\mathcal{A}\). Hence we can find a realizer \(r\) uniform to \(X\) such that \(r\Vdash^f \lnot\lnot(a_X=1)\), so we can find another realizability \(r'\) satisfying \(r'\Vdash^f a_X\in \operatorname{WDec}(1)\) for all nonempty \(X\subseteq\mathcal{A}\) by 3. Now assume that \(b\in V^f(\mathcal{A})\) and \(e\in\mathcal{A}\) satisfy \[e\Vdash^f \forall x [x\subseteq \operatorname{WDec}(1) \to x\in b].\] Then for any inhabited \(X\subseteq \mathcal{A}\), \(e(\lambda f.\mathbf{p0i_r})\Vdash^f a_X\in b\). Thus for each inhabited \(X\subseteq \mathcal{A}\) we can find \(\langle(e(\lambda f.\mathbf{p0i_r}))_0,c \rangle\in b\) such that \((e(\lambda f.\mathbf{p0i_r}))_1\Vdash^f a_X=c\). By functionality of \(b\), \(c\) does not depend on \(X\). Hence we can find a realizer \(\alpha\), which does not depend on \(X, Y\subseteq \mathcal{A}\), such that \(\alpha\Vdash a_X=a_Y\).

Now observe that \(\alpha\Vdash a_X=a_Y\) implies \((\alpha)_0\Vdash a_X\subseteq a_Y\). By unpacking it, we have \[\forall \langle f,\varnothing\rangle \in a_X \exists \langle (\alpha f)_0, \varnothing\rangle \in a_Y [(\alpha f)_1 \Vdash^f \varnothing=\varnothing].\]

Hence \(f\mapsto (\alpha f)_0\) is a function from \(X\) to \(Y\), regardless of what \(X\) and \(Y\) are. This leads to a contradiction if we take, say, \(X=\{\mathbf{k}\}\), \(Y=\{\mathbf{k}\}\) and \(Y=\{r\}\) for some \(r\in\mathcal{A}\), \(r\neq \mathbf{k}\). Then the map \(f\mapsto (\alpha f)_0\) sends \(\mathbf{k}\) to \(\mathbf{k}\) and \(r\), which is impossible. ◻