Proof. Suppose there is $A\in \Sigma _{1}^{M}(M)$ is such that $A\subset \mathbb {P}$ is an antichain in $\mathbb {P}$ which is unbounded in $\delta $ . Since $\mathbb {P}$ has the $\delta $ -c.c. in M, and $\delta $ is regular in M, this means that $A\notin M$ . Let $\varphi $ be a $\Sigma _{1}$ -formula such that for some $p\in M$ ,

$$\begin{align*}x\in A\iff M\models\varphi(x,p). \end{align*}$$

Define for $\alpha <\operatorname {\mathrm {OR}}^{M}\setminus \delta $ such that $p\in M\vert \alpha $ ,

$$\begin{align*}A_{\alpha}:=\{\xi\in\delta:M\vert\alpha\models\varphi(\xi,p)\}. \end{align*}$$

Note that $A=\bigcup _{\alpha <\operatorname {\mathrm {OR}}^{M}}A_{\alpha }$ and $A_{\alpha }\in M$ for all $\alpha $ such that $\alpha \in \operatorname {\mathrm {OR}}^{M}\setminus \delta $ and ${p\in M\vert \alpha} $ . In particular, since $A_{\alpha }\subset A$ is an antichain, $\mathbb {P}$ has the $\delta $ -c.c. in M, and $\delta $ is regular in M, $A_{\alpha }$ is bounded in $\delta $ for all such $\alpha $ .

Note that since $A=\bigcup _{\alpha <\operatorname {\mathrm {OR}}^{M}}A_{\alpha }$ is by assumption unbounded in $\delta $ ,

$$\begin{align*}M\models\forall\beta<\delta\exists\alpha(\exists\gamma(\gamma>\beta\land\gamma\in A_{\alpha})). \end{align*}$$

Since the last part of this formula is $\Sigma _{1}$ , we have by $\Delta _{0}$ -collection that there is some $\alpha ^{\prime }\in M$ such that $\alpha ^{\prime }$ works for all $\beta <\delta $ uniformly, i.e.

$$\begin{align*}M\models\exists\alpha^{\prime}\forall\beta<\delta(\exists\gamma(\gamma>\beta\land\gamma\in A_{\alpha^{\prime}})). \end{align*}$$

This contradicts the fact that every $A_\alpha $ is bounded in $\delta $ !

Proof. We construct the set A recursively along the ordinals of M. More specifically, we will define via a $\Sigma _{1}$ -recursion a sequence $\langle (A^{i},\beta _{i}):i<\operatorname {\mathrm {OR}}^{M}\rangle $ with each $A^i \in M$ and $\beta _i \in \operatorname {\mathrm {OR}}^M$ , and $\langle (A^i,\beta _i) : i< \lambda \rangle \in M$ for each $\lambda <\operatorname {\mathrm {OR}}^M$ . We will then set $A=\bigcup _{i<\operatorname {\mathrm {OR}}^{M}}A^{i}$ . Let $\beta _{0}$ be the least $\beta $ such that

$$\begin{align*}M\vert\beta\models\exists\alpha<\lambda\exists p\in\mathbb{P}(\exists\dot{x}\in M^{\mathbb{P}}(p\Vdash_{M\vert\beta}^{\mathbb{P}}\psi(\dot{x},\check{\alpha},\dot{z}))), \end{align*}$$

i.e., $\beta $ is such that there is some $\alpha <\lambda $ such that $W_{\varphi ,\check {\alpha },\dot {z}}^{ M\vert \beta }\neq \emptyset $ . Let $A^{0}$ be the set of all $(\alpha ,p)\in A^{0}$ such that $\alpha <\lambda $ , $W_{\varphi ,\check {\alpha },\dot {z}}^{M\vert \beta _0} \neq \emptyset $ , and p is the $<_{M}$ -least element in $W_{\varphi ,\check {\alpha },\dot {z}}^{M\vert \beta _0}$ . Here, $<_{M}$ denotes the canonical $\Sigma _{1}$ -definable well-order of M. Note that $A^{0}\in M$ , since it is definable over $M \vert \beta _0$ . Moreover, $A^{0}$ is a bounded subset of $\delta $ . (Actually, of $\delta ^{2}$ , but via coding we may assume that $A^{0}\subset \delta $ ). Before we continue the construction let us introduce the following notation: For $\alpha <\lambda $ and $i<\operatorname {\mathrm {OR}}^{M}$ let $A_{\alpha }^{i}:=\{q\in \mathbb {P}:(\alpha ,q)\in A^{i}\}$ , where $A^{i}$ is to be defined.

Let $\gamma +1<\operatorname {\mathrm {OR}}^{M}$ and suppose that $\langle (A^{i},\beta _{i}):i\leq \gamma \rangle $ is defined such that $\langle (A^{i},\beta _{i}):i\leq \gamma \rangle \in \Sigma _{1}^{M}(\{\lambda ,\psi ,\dot {z},\mathbb {P}\})$ . We define $\beta _{\gamma +1}$ as the least $\beta $ such that

$$\begin{align*}M\vert\beta\models\exists\alpha<\lambda\exists p\in\mathbb{P}((\forall q\in A_{\alpha}^{\gamma}(p\perp q))\land p\in W_{\varphi,\check{\alpha},\dot{z}}), \end{align*}$$

if there is such $\beta $ . In other words $\beta $ is such that for some $\alpha $ there is an element $p\in W_{\varphi ,\check {\alpha },\dot {z}}^{M\vert \beta }$ incompatible with the elements of $A_{\alpha }^{\gamma }$ . In case $\beta _{\gamma +1}$ is undefined we stop the recursion. Note that in this case $A^{\gamma }\in M$ .

In case $\beta _{\gamma +1}$ is defined, we set $A^{\gamma +1}$ to be the union of $A^{\gamma }$ with the set of all $(\alpha ,p)$ such that p is the $<_{M}$ -least q such that

$$\begin{align*}M\vert\beta_{\gamma+1}\models q\in W_{\varphi,\check{\alpha},\dot{z}}\land\forall r\in A_{\alpha}^{\gamma}(r\perp q), \end{align*}$$

if there is such q. Since $A^{\gamma +1}$ is definable over $M\vert \beta _{\gamma +1}$ , $A^{\gamma +1}\in M$ .

Now suppose that $\gamma <\operatorname {\mathrm {OR}}^{M}$ is a limit ordinal and $\langle A^{i}:i<\gamma \rangle $ is defined. We set $\beta _{\gamma }=0$ and $A^{\gamma }=\bigcup _{i<\gamma }A^{i}$ . Note that since $\langle A_{i}:i<\gamma \rangle \in \Sigma _{1}^{M}(M)$ by KP, $A^{\gamma }\in M$ .

We aim to see that the recursive definition of $\langle (A^{i},\beta _{i}):i<\operatorname {\mathrm {OR}}^{M}\rangle $ stops before the ordinal height of $\operatorname {\mathrm {OR}}^{M}$ , i.e. there is some $\gamma <\operatorname {\mathrm {OR}}^{M}$ such that $\beta _{\gamma }$ is not defined. Suppose that this is not the case. We claim that $\bar {A}:=\bigcup _{i<\operatorname {\mathrm {OR}}^{M}}A^{i}\in \Sigma _{1}^{M}(M)$ is an unbounded subset of $\delta $ . For suppose not. Then, since $\rho _{1}^{M}=\delta $ , $\bar {A}\in M$ . But the definition of $\bar {A}$ gives a cofinal and total $f:\bar {A}\rightarrow \operatorname {\mathrm {OR}}^{M}$ such that $f\in \Sigma _{1}^{M}(M)$ . Contradiction!

In particular, the following holds in M,

$$\begin{align*}\forall\beta<\delta\exists(\alpha,\gamma)(\alpha<\lambda\land\gamma\in(\beta,\delta)\land\exists\beta_{i}("\gamma\text{ is added to }A_{\alpha}\text{ at stage }\beta_{i}")). \end{align*}$$

But by $\Delta _{0}$ -collection, there is some $\beta _{i}<\operatorname {\mathrm {OR}}^{M}$ such that for all $\beta <\delta $ , there is some $\gamma \in (\beta ,\delta )$ added to $A_{\alpha }^{i}$ for some $\alpha <\lambda $ . But this is inside $M\vert \beta _{i}+\omega $ . Thus, as $\delta $ is a regular cardinal of M, there is some $\alpha $ to which unboundedly many $\gamma <\delta $ are added. Contradiction, since $\mathbb {P}$ has the $\delta $ -c.c. in M.

Let $\gamma <\operatorname {\mathrm {OR}}^{M}$ be least such that $\beta _{\gamma }$ is undefined. Note that $\gamma $ is by definition a successor ordinal, i.e. $\gamma =\eta +1$ for some $\eta <\operatorname {\mathrm {OR}}^{M}$ . Set $A:=A^{\eta }$ . By construction $A\in M$ . For $\alpha <\lambda $ , set $A_{\alpha }:=\{p\in \mathbb {P}:(\alpha ,p)\in A\}$ . Since $\beta _{\eta +1}$ is undefined, we have that for all $\alpha <\lambda $ , $A_{\alpha }\subset W_{\varphi ,\check {\alpha },\dot {z}}$ is a maximal antichain in $W_{\varphi ,\check {\alpha },\dot {z}}$ .

Proof. We will verify that $M[g]$ satisfies $\Delta _{0}$ -collection and leave the remaining axioms of KP as an exercise.

Let $g\subset \mathbb {P}$ be M-generic and suppose for the sake of contradiction that $M[g]\not \models "\Delta _{0}\text {-collection}"$ . Let $\psi $ be a $\Sigma _{0}$ -formula and $y\in M[g]$ such that they constitute a counterexample to $\Delta _{0}$ -collection, i.e.

$$\begin{align*}M[g]\models\forall\alpha<\delta\exists x(\psi(\alpha,x,y)), \end{align*}$$

but there exists no $z\in M[g]$ such that

$$\begin{align*}M[g]\models\forall\alpha<\delta\exists x\in z(\psi(\alpha,x,y)). \end{align*}$$

We distinguish two cases. First, suppose that there is some $\lambda <\delta $ such that there exists no $z\in M[g]$ such that

$$\begin{align*}M[g]\models\forall\alpha<\lambda\exists x\in z(\psi(\alpha,x,y)). \end{align*}$$

Then, by the previous Lemma 9 there is $A\in M$ such that for $\alpha <\lambda $ , $A_{\alpha }:=\{p\in \mathbb {P}:(\alpha ,p)\in A\}$ is a maximal antichain in $W_{\varphi ,\check {\alpha },\dot {y}}$ , where $\varphi \equiv \exists x\psi $ and $\dot {y}\in M^{\mathbb {P}}$ is a $\mathbb {P}$ -name for y.

We have established that for all $\alpha <\lambda $ , $A_{\alpha }\cap g\neq \emptyset $ . Moreover, by Theorem 8, we have that

$$\begin{align*}M\models\forall a\in A\exists\dot{x}(\exists p\in\mathbb{P}\exists\alpha<\lambda(a=(\alpha,p)\land p\Vdash_{M}^{\mathbb{P}}\psi(\check{\alpha},\dot{x},\dot{y}))). \end{align*}$$

This is the antecedence of an instance of the $\Delta _{0}$ -collection scheme since the part in parentheses is $\Sigma _{1}$ (note that we are using here the fact that $\Vdash _{M}^{\mathbb {P}}$ for $\Sigma _{1}$ statements is $\Sigma _{1}$ definable over M which is true by Theorem 8). Thus, there is $z\in M$ such that

$$\begin{align*}M\models\forall a\in A\exists\dot{x}\in z(\exists p\in\mathbb{P}\exists\alpha<\lambda(a=(\alpha,p)\land p\Vdash_{M}^{\mathbb{P}}\psi(\check{\alpha},\dot{x},\dot{y}))). \end{align*}$$

Let $z^{g}:=\{\dot {x}^{g}:x\in z\cap M^{\mathbb {P}}\}$ . Note that $z^{g}\in M[g]$ , as $z\cap M^{\mathbb {P}}\in M\cap M^{\mathbb {P}}$ . It follows that

$$\begin{align*}M[g]\models\forall\alpha<\lambda\exists x\in z^{g}(\psi(\alpha,x,y)), \end{align*}$$

a contradiction!

Let us now turn towards the second case, i.e., we assume that for all $\lambda <\delta $ there is $z\in M[g]$ such that

$$\begin{align*}M[g]\models\forall\alpha<\lambda\exists x\in z(\psi(\alpha,x,y)). \end{align*}$$

Let us associate to $\psi $ a function $f\in \Sigma _{1}^{M[g]}(M[g])$ such that $f:\delta \rightarrow \operatorname {\mathrm {OR}}^{M[g]}$ and for $\alpha <\delta $ , $f(\alpha )$ is the least $\beta $ such that there is $x\in M\vert \vert \beta [g]$ such that $M[g]\models \psi (\alpha ,x,y)$ . By our assumption $f\!\upharpoonright \!\alpha \in M[g]$ for every $\alpha <\delta $ , but $f\notin M[g]$ . Let us define an auxiliary function F with domain $\delta $ such that $F(\alpha )=f\!\upharpoonright \!\alpha $ . Note that $F\in \Sigma _{1}^{M[g]}(M[g])$ . Let $\varphi ^\prime _{F}$ be a $\Sigma _1$ formula and $z\in M[g]$ such that

$$\begin{align*}(c,d)\in F\iff M[g]\models\varphi^\prime_{F}(c,d,z), \end{align*}$$

and let $\varphi _F(a,b,z)$ be the formula

(2.1) $$ \begin{align} \exists c \exists d (\varphi^\prime_F (c,d,z) \land a \leq c \land b = d \!\upharpoonright\! a). \end{align} $$

Let

$$\begin{align*}X:=\{p\in\mathbb{P}:\exists\beta<\operatorname{\mathrm{OR}}^{M}(p\Vdash_{M\vert\beta}^{\mathbb{P}}\forall\alpha<\check{\delta}\exists y\varphi_{F}(\alpha,y,\dot{z}))\}. \end{align*}$$

Note that $X\in \Sigma _{1}^{M}(M)$ and let $\varphi _{X}$ be the defining formula and $a\in M$ the corresponding parameter.

We now aim to construct in a similar way as in the proof of Lemma 9 a maximal antichain A in X. If $X \neq \emptyset $ , let $A_{0}:=\{p\}$ for some $p\in X$ . Otherwise, set $A_0 = \emptyset $ . Suppose that $\langle A_{i}:i<\gamma \rangle $ is defined via a $\Sigma _{1}$ -recursion for some $\gamma <\operatorname {\mathrm {OR}}^{M}$ . If $\gamma $ is a limit ordinal, let $A_{\gamma }=\bigcup _{i<\gamma }A_{i}$ . Then, $A_{\gamma }\in M$ and $\langle A_{i}:i\leq \gamma \rangle \in \Sigma _{1}^{M}(M)$ . If $\gamma $ is not a limit, let $\beta _{\gamma }<\operatorname {\mathrm {OR}}^{M}$ be the least $\beta $ such that

$$\begin{align*}M\vert\beta\models\exists p\in\mathbb{P} (\varphi_{X}(p,a) \land \forall q\in A_{\gamma-1}(q \perp p)), \end{align*}$$

if there exists such $\beta $ . In the case that there is no such $\beta $ , stop the recursion. In case $\beta _{\gamma }$ is defined, let $p_{\gamma }$ be the $<_{M}$ -least p such that

$$\begin{align*}M\vert\beta_{\gamma}\models \varphi_{X}(p,a) \land \forall q\in A_{\gamma-1} (q\perp p). \end{align*}$$

Let $A_{\gamma }:=A_{\gamma -1}\cup \{p_{\gamma }\}$ . It is not hard to verify that $\langle A_{i}:i\leq \gamma \rangle \in \Sigma _{1}^{M}(M)$ and ${A_{\gamma }\in M}$ .

Similar to the proof of the Lemma 9 we aim to see that there is a least $\gamma <\operatorname {\mathrm {OR}}^{M}$ such that $\beta _{\gamma }$ is undefined, which will show that $A:=A_{\gamma -1}$ is a maximal antichain in X and $A\in M$ .

Suppose for the sake of contradiction that for all $\gamma <\operatorname {\mathrm {OR}}^{M}$ , $\beta _{\gamma }$ is defined. Let $\bar {A}:=\bigcup _{\gamma <\operatorname {\mathrm {OR}}^{M}}A_{\gamma }$ . Clearly, $\bar {A}\in \Sigma _{1}^{M}(M)$ . Since $\bar {A}$ is by construction an antichain, by Lemma 5 $\bar {A}$ is bounded in $\delta $ . In particular, $\bar {A}\in M$ . However, as in the previous proof, the definition of $\bar {A}$ give rise to a function $f\in \Sigma _{1}^{M}(M)$ such that $\operatorname {\mathrm {dom}}(f)=\bar {A}$ and f is cofinal in $\operatorname {\mathrm {OR}}^{M}$ . But this is a contradiction!

Let $D:=\{p\in \mathbb {P}:\forall q\in A(q\perp p)\}$ . As $A\in M$ , $D\in M$ and thus, $A\cup D\in M$ . $A\cup M$ is pre-dense and therefore, $g\cap (A\cup D)\neq \emptyset $ . Note that $g\cap A=\emptyset $ , so ${g\cap D\neq \emptyset} $ .

Let $\tilde {p}\in D\cap g$ . Note that this means that there is no extension p of $\tilde {p}$ such that

(2.2) $$ \begin{align} p\Vdash_{M}^{w.\mathbb{P}} \exists \beta ((M \vert \beta) [\dot{g}]\models \forall\alpha<\check{\delta}\exists y\varphi_{F}(\alpha,y,\dot{z})). \end{align} $$

We claim that there is $\vec {p} = \langle p_{i}:i<\delta \rangle \in M$ such that for all $i < \delta $ , $p_i \leq \tilde {p}$ and $M \models \psi (i,\dot {z},p_i)$ , where $\psi (i,\dot {z},p)$ is the statement

(2.3) $$ \begin{align} p\Vdash_{M}^{w.\mathbb{P}}\exists y\varphi_{F}(i,y,\dot{z}). \end{align} $$

We may find such $\langle p_{i}:i<\delta \rangle $ in M, as $\Delta _{0}$ -collection holds in M and

$$\begin{align*}M\models\forall i<\delta\exists p((p\Vdash_{M}^{w.\mathbb{P}}\exists y\varphi_{F}(i,y,\dot{z}))\land p\leq\tilde{p}). \end{align*}$$

For every $i<\delta $ there exists such $p\in \mathbb {P}$ , since $\tilde {p}\in g$ and $M[g]\models \forall i<\delta \exists y\varphi _{F}(i,y,z)$ and so by Theorem 8 the existence of p follows.

Now since $p_{i_0}\leq \tilde {p}$ , the following claim gives a contradiction, completing the proof:

As stated prior the claim, this completes the proof.

Proof. Note that $\mathbb {\mathbb {C}_{\delta }}\in M$ is such that

$$\begin{align*}M\models "\mathbb{C}_{\delta}\text{ is a }<\delta\text{-closed, separable, and atom-less forcing}". \end{align*}$$

By Lemma 4 and $1$ -soundness, $\delta =\rho _{1}^{M}$ and $M=H_{1}^{M}(\delta \cup \{p_{1}^{M}\})$ . Thus, there is a partial surjective function $h:\delta \rightarrow M$ such that $h\in \Sigma _{1}^{M}(\{p_{1}^{M}\})$ . Let

$$\begin{align*}\tilde{D}:=\{\xi<\delta:M\models "h(\xi)\subset\mathbb{C}_{\delta}\text{ is dense in }\mathbb{C}_{\delta}"\}. \end{align*}$$

Note that $\tilde {D}\notin M$ , as otherwise M could construct an M-generic. Let

$$\begin{align*}D:=\langle\xi_{i}:i<\delta\rangle, \end{align*}$$

be the monotone enumeration of $\tilde {D}$ . Note that $\tilde {D}$ has ordertype $\delta $ . Since $h\in \Sigma _{1}^{M}(M)$ , $\tilde {D}\in \Sigma _{1}^{M}(M)$ . However, $D\notin \Sigma _{1}^{M}(M)$ , as otherwise by $\Delta _{0}$ -collection, $D\in M$ .

The idea is now to construct an M-generic g which codes in a $\Sigma _{1}$ -fashion the set D so that $D\in M[g]$ if $(\lfloor M[g] \rfloor , \in ) \models \text {KP}$ .

Let us define $\tilde {g} = \langle p_{i}:i<\delta \rangle $ via a recursion on i such that for all $\alpha < \delta $ , $\langle p_{i}:i<\alpha \rangle $ is uniformly $\Sigma _1$ over M in the parameters $\{D\!\upharpoonright \! \alpha , \mathbb {C}_\delta \}$ . We will have that $p_{i}\leq p_{j}$ for $j<i$ . Set $p_{0}:=\langle \xi _{0}\rangle $ and $p_{1}$ to be the $<_{M}$ -least $p\in h(\xi _{0})$ such that $p\leq p_{0}$ . Note that there is such p, since $h(\xi _{0})$ is dense in $\mathbb {C}_{\delta }$ .

Suppose that $\langle p_{i}:i<\lambda \rangle $ is defined, where $\lambda <\delta $ is a limit ordinal, such that $p_{i}\leq p_{j}$ for $j\leq i<\lambda $ . Note that $D\!\upharpoonright \!\lambda \in M$ , since $\tilde {D}\in \Sigma _{1}^{M}(M)$ and $\delta $ is $\Sigma _{1}^M (M)$ -regular by Lemma 6. By our induction hypothesis the construction so far is uniformly $\Sigma _{1}$ in the parameters $D\!\upharpoonright \!\lambda $ and $\mathbb {C}_{\delta }$ . This implies that $\langle p_{i}:i<\lambda \rangle \in M$ . Thus, we can set $p_{\lambda }=(\bigcup _{i<\lambda }p_{i})^{\frown }\langle \xi _{\lambda }\rangle $ . Let $p_{\lambda +1}$ be the $<_{M}$ -least $p\in h(\xi _{\lambda })$ such that $p\leq p_{\lambda }$ .

We now turn towards the successor case. Suppose we have defined $\langle p_\beta \rangle _{\beta \leq \gamma }$ where $\gamma $ is an odd successor (that is, $\gamma =\lambda +2n+1$ for some $n<\omega $ and $\lambda $ is a limit less than $\gamma $ or equal to $0$ ). Set $p_{\gamma + 1} := p_{\gamma }^{\frown }\langle \xi _{\lambda +n}\rangle $ and let $p_{\gamma + 2}$ be the $<_{M}$ -least $p\in h(\xi _{\lambda +n})$ such that $p\leq p_{\gamma +1}$ .

Let g be the upwards-closure of $\tilde {g}$ in $\mathbb {\mathbb {C}_{\delta }}$ . By definition of $\tilde {g}$ , g is M-generic. Note that since $\mathbb {E}^{M}\!\upharpoonright \!\delta \in M[g]$ by Lemma 12 we can define $\mathbb {E}^{M}$ over $M[g]$ in a $\Sigma _{1}$ fashion as the extender sequence of the stack of sound premice extending $M\vert \delta $ which project to $\delta $ and for which condensation holds. Thus, it follows that ${(M, \in , \mathbb {E}^M) \in \Sigma _{1}^{(\lfloor M[g] \rfloor , \in )}(\{ M \vert \delta \})}$ . Note that therefore $\tilde {g}$ is definable over $(M[g], \in )$ from $\{\mathbb {C}_{\delta },\delta ,g, M \vert \delta \}$ via a $\Sigma _{1}$ recursion of length $\delta $ . Thus, if $(\lfloor M[g] \rfloor , \in ) \models \text {KP}$ , then $\tilde {g} \in M[g]$ and so $D \in M[g]$ .

Let $h^{\prime }:\delta \rightarrow \operatorname {\mathrm {OR}}^{M}$ be the partial function such that $h^{\prime }(\alpha )$ is the least ${\beta <\operatorname {\mathrm {OR}}^{M}}$ such that $h(\alpha )\in M \vert \beta $ , if $h(\alpha )$ is defined. Clearly, $h^{\prime }\in \Sigma _{1}^{M}(\{p_{1}^{M}\})$ . We have that $h^{\prime }\in \Sigma _{1}^{(\lfloor M[g] \rfloor , \in )}(\lfloor M[g] \rfloor )$ . Moreover, as $\mathbb {C}_{\delta }$ is $<\delta $ -closed and atom-less, ${\operatorname {\mathrm {ran}}(h^{\prime }\!\upharpoonright \! D)}$ is cofinal in M. Since $\operatorname {\mathrm {OR}}^{M}=\operatorname {\mathrm {OR}}^{M[g]}$ , $h^\prime \!\upharpoonright \! D$ is cofinal in $M[g]$ . But now if $(\lfloor M[g] \rfloor , \,{\in}) \models \text {KP,}$ since $D\in M[g]$ , $\operatorname {\mathrm {OR}}^{M[g]}\in M[g]$ . Contradiction! Thus, ${(\lfloor M[g] \rfloor , \in ) \not \models \text {KP}}$ .

Proof. We prove the two directions separately.

Proof. Note that in the case that $\deg ^{\mathcal {T}}(\theta )\geq 2$ , the lemma holds by Lemma 14. Thus, we may assume that $\deg ^{\mathcal {T}}(\theta ) \leq 1$ .

By standard facts $\mathcal {M}_{\theta }^{\mathcal {T}}$ is a passive premouse with a largest, regular, and uncountable cardinal. We have to verify that $\mathcal {M}_{\theta }^{\mathcal {T}}$ is admissible. By Lemma 3, it suffices to show that $\Delta _{0}$ -collection holds in $\mathcal {M}_{\theta }^{\mathcal {T}}$ .

Case 1. $\theta = \zeta + 1$ is a successor ordinal.

We inductively assume that $\mathcal {M}^{*\mathcal {T}}_{\theta }$ is an admissible passive premouse with a largest, regular, and uncountable cardinal.

Let $n := \deg ^{\mathcal {T}} (\theta )$ , $M:= \mathcal {M}^{*\mathcal {T}}_\theta $ , $E:=E_{\zeta }^{\mathcal {T}}$ , and $M^\prime := \text {Ult}_{n}(\mathcal {M}_\theta ^{*\mathcal {T}},E)$ . By our initial remarks $n \leq 1$ . By standard arguments $\kappa := \operatorname {\mathrm {crit}}(E)$ is strictly less than the largest cardinal of M. In particular, by Lemma 4, $\kappa < \rho _1^M$ .

Since M is admissible we have by $\Delta _{0}$ -collection that for any $m<\omega $ , $f\in \Sigma _{1}^{M}(M)\cap {^{[\kappa ]^{m}}M}$ implies that $f\in M$ . This means that the canonical factor map $\pi \colon \text {Ult}_{0}(M,E) \to \text {Ult}_{1}(M,E)$ is the identity. Thus, $\text {Ult}_{0}(M,E)=\text {Ult}_{1}(M,E)$ and the associated ultrapower maps are the same. In particular, $i^{*\mathcal {T}}_{\theta }\colon M\to M^{\prime }$ is a $1$ -embedding and $i^{*\mathcal {T}}_{\theta }$ is cofinal in $\operatorname {\mathrm {OR}}^{M^{\prime }}$ .

Subclaim 1. For $a \in [\operatorname {\mathrm {lh}}(E)]^{<\omega }$ , $\text {Ult}_{0}(M,E_a) \models \text {KP}$ .

Proof. Let $a \in [\operatorname {\mathrm {lh}}(E)]^{<\omega }$ and suppose for contradiction that ${\text {Ult}_{0}(M,E_a) \not \models \text {KP}}$ . By our initial remarks this means that $\Delta _{0}$ -collection fails in $\text {Ult}_{0}(M,E_a)$ , i.e., there is a $\Sigma _{0}$ -formula $\varphi $ , $\xi < \operatorname {\mathrm {OR}}^{\text {Ult}_{0}(M,E_a)}$ , and $p\in \text {Ult}_{0}(M,E_a)$ such that

(2.4) $$ \begin{align} \text{Ult}_{0}(M,E_a) \models\forall\alpha<\xi\exists x\varphi(\alpha,x,p), \end{align} $$

but there is no $z\in \text {Ult}_{0}(M,E_a)$ such that

(2.5) $$ \begin{align} \text{Ult}_{0}(M,E_a) \models\forall\alpha<\xi\exists x\in z\varphi(\alpha,x,p). \end{align} $$

Let $i \colon M \to \text {Ult}_{0}(M,E_a)$ be the ultrapower embedding. By our previous remarks we have that i is a $1$ -embedding and cofinal in $\operatorname {\mathrm {OR}}^{\text {Ult}_{0}(M,E_a)}$ .

Let $\delta $ be the largest cardinal of M and $\delta ^{\prime }=i(\delta )$ be the largest cardinal of $\text {Ult}_{0}(M,E_a)$ . By Lemma 3 we may assume that $\xi $ in (2.4) is equal to $\delta ^{\prime }$ . Let $j=\lvert a\rvert $ . Let $g^{\prime }\colon \delta ^\prime \to \text {Ult}_{0}(M,E_a)$ be the canonical function derived from $\varphi $ by taking the $<_{\text {Ult}_{0}(M,E_a)}$ -least witness. Note that $g^{\prime }\in \Sigma _{1}^{\text {Ult}_{0}(M,E_a)}(\{p\})$ as $\varphi $ is $\Sigma _{0}$ . We will now show that $g^\prime $ is bounded in $\text {Ult}_{0}(M,E_a)$ . This will contradict the failure of $\Delta _0$ -collection, completing the proof.

By the definition of $\text {Ult}_{0}(M,E_a)$ we have for $\alpha <\delta ^{\prime }$ some $f_{\!\alpha } \in {^{[\kappa ]^{j}}}\delta \cap M$ such that $\alpha =[a,f_{\!\alpha }]_{E_a}^{M}$ . Also, there is $f_{\!\!p}\in ({^{[\kappa ]^{j}}}M) \cap M$ such that $p=[a,f_{\!\!p}]_{E}^{M}$ . Since we assumed that $\delta $ is regular in M and $\kappa < \delta $ we may assume that for $\alpha <\delta ^\prime $ , $f_{\!\alpha }\in {^{[\kappa ]^{j}}}\delta \cap (M\vert \delta )$ . Moreover, since Łoś’s Theorem holds for $\Sigma _{1}$ -formulae, we have by (2.4) for all $\alpha <\delta ^{\prime }$ ,

$$\begin{align*}A_{\alpha}:=\{b\in[\kappa]^{j}:M\models\exists x\varphi(f_{\!\alpha}(b),x,f_{\!\!p}(b))\}\in E_a. \end{align*}$$

Note that for any $h\in {^{[\kappa ]^{j}}} \delta \cap (M\vert \delta )$ there is some $\alpha <\delta ^{\prime }$ such that $\alpha =[a,h]_{E}^{M}$ . Thus,

$$\begin{align*}M\models\forall h\in {^{[\kappa]^{j}}}\delta\cap(M\vert\delta)\exists A(A\in E_a \land\forall b\in A\exists x\varphi(h(b),x,f_{\!\!p}(b))). \end{align*}$$

Note that this does make sense since $E_a \in M$ : By standard facts about k-maximal iteration trees E is close to M and therefore in particular, for every $b \in [\operatorname {\mathrm {lh}}(E)]^{<\omega }$ , $E_{b} \in \Sigma _{1}^{M}(M)$ . But since M is admissible and $\kappa < \delta $ , this implies that $E_a \in M$ .

Using $\Delta _{0}$ -collection, we have for every $h\in {^{[\kappa ]^{j}}} M \cap (M\vert \delta )$ and A such that

$$\begin{align*}M \models A \in E_a \land\forall b\in A\exists x\varphi(h(b),x,f_{\!\!p}(b)), \end{align*}$$

there is some $Y\in M$ such that

$$\begin{align*}M\models A \in E_a \land\forall b\in A\exists x\in Y\varphi(h(b),x,f_{\!\!p}(b)). \end{align*}$$

Thus,

$$\begin{align*}M\models\forall h\in {^{[\kappa]^{j}}}\delta\cap(M\vert\delta)\exists A\exists Y(A\in E_a \land\forall b\in A\exists x\in Y\varphi(h(b),x,f_{\!\!p}(b))). \end{align*}$$

By another application of $\Delta _{0}$ -collection this gives us $\beta < \operatorname {\mathrm {OR}}^M$ such that

$$\begin{align*}M\models\forall h\in {^{[\kappa]^{j}}}\delta\cap(M\vert\delta)\exists A\in E_a (\forall b\in A\exists x\in (M \vert \beta)\varphi(h(b),x,f_{\!\!p}(b))). \end{align*}$$

It now easily follows that $g^{\prime }$ is bounded by $M^\prime \vert i(\beta )$ .

In the case that E is finitely generated this argument shows that $M^\prime \models \text {KP}$ . Thus, we may assume that E is not finitely generated. In this case, $M^{\prime }$ is the direct limit of

$$\begin{align*}(\text{Ult}_{0}(M,E_{a}),\pi_{ab}:a,b\in[\nu(E)]^{<\omega}\land a\subset b), \end{align*}$$

where $\pi _{ab}$ is the canonical factor embedding. For $a\in [\nu (E)]^{<\omega }$ let $X_{a}:=\pi _{a\infty }[\text {Ult}_{0}(M,E_{a})]$ . By Łoś’s Theorem it follows that $\pi _{a\infty }:\text {Ult}_{0}(M,E_{a})\rightarrow M^{\prime }$ is $\Sigma _{1}$ -elementary.

Suppose now that $f ^\prime \in \Sigma _{1}^{M^{\prime }} (M^{\prime })$ . There is some $a \in [\nu (E)]^{<\omega }$ such that ${f^\prime \in \Sigma _1^{M^\prime } (\{ p^\prime \})}$ for some $p^\prime \in X_{a}$ . Let $p = \pi _{a \infty }^{-1}(p^\prime )$ and let f be the function, which is defined over $\text {Ult}_{0}(M,E_a)$ via the parameter p, as $f^\prime $ is defined over $M^\prime $ via the parameter $p^\prime $ . By the claim we have that $f \in \text {Ult}_{0}(M,E_a)$ . But this means that $f^\prime \in M^\prime $ . Thus, by Lemma 3, $M^\prime $ is admissible.

Case 2. $\operatorname {\mathrm {lh}}(\mathcal {T}) = \theta $ is a limit ordinal.

This is proven much as in the case that $\theta = \zeta +1$ is a successor ordinal and $E_\zeta $ is not finitely generated.

This finishes the proof of Claim 1.

Proof. Again we argue by induction on $\theta $ . Suppose first that $\theta =\zeta +1$ and let $\mathcal {M}^{\mathcal {T}}_\theta = M^\prime $ and $M = \mathcal {M}_\theta ^{*\mathcal {T}}$ . Again, by standard arguments we may assume that M is a premouse with a largest, regular, and uncountable cardinal $\delta $ . It suffices to see that M is admissible for which in turn it suffices to see that $\Delta _0$ -collection holds in M. Suppose for the sake of contradiction that this is not true and let $\eta < \operatorname {\mathrm {OR}}^M$ witness the least failure of $\Delta _{0}$ -collection, i.e.,

1. 1. there is a $\Sigma _{1}$ -formula $\varphi $ and $p\in M$ such that $M\models \forall \alpha <\eta \exists x\varphi (x,\alpha ,p)$ , but there is no $z\in M$ such that $M\models \forall \alpha <\eta \exists x\in z\varphi (x,\alpha ,p)$ , and

2. 2. for all $\Sigma _1$ -formulas $\psi $ and $q \in M$ we have that if $\gamma < \eta $ and $M \models \forall \alpha < \gamma \exists x \psi (x,q)$ , then there is $z \in M$ such that $M \models \forall \alpha < \gamma \exists x \in z \psi (x,q)$ .

Let $n = \deg _\theta ^{\mathcal {T}}$ so that $M^\prime = \text {Ult}_{n}(M,E)$ , where $E = E_{\zeta }^{\mathcal {T}}$ . As before we may assume that $n\leq 1$ . Let $i:=i_{\theta }^{*\mathcal {T}}:M\rightarrow M^{\prime }$ be the ultrapower map and let $\delta ^{\prime }=i(\delta )$ be the largest cardinal of $M^{\prime }$ . Note that we can no longer assume that i is both a $0$ - and a $1$ -embedding, unlike in Claim 1.

Case 1. $n=1$ .

Note that it suffices to see that $M^{\prime }\models \forall \alpha <i(\eta )\exists x \varphi (x,\alpha ,i(p))$ because then by the admissibility of $M^{\prime }$ , $M^{\prime }\models \exists z^{\prime }\forall \alpha <i(\eta )\exists x\in z^{\prime }\varphi (x,\alpha ,i(p))$ and so by the elementarity of i there is a bound in M. Note that i is a $1$ -embedding and therefore $r\Sigma _2$ -elementary. But this means that $M^{\prime }\models \forall \alpha <i(\eta )\exists x \varphi (x,\alpha ,i(p))$ .

Case 2. $n=0$ .

Let $\eta ^{\prime }:=\sup (i[\eta ])$ and note that $\eta ^{\prime }$ is a limit ordinal. We claim that for every $\alpha < \eta ^\prime $ , $M^\prime \models \exists x \varphi (x,\alpha ,i(p))$ . Suppose otherwise and let $\alpha ^{\prime }<\eta ^{\prime }$ be a counterexample, i.e.

$$\begin{align*}M^{\prime}\models\forall x\neg\varphi(x,\alpha^{\prime},i(p)). \end{align*}$$

Let $\alpha <\eta $ be such that $i(\alpha )>\alpha ^{\prime }$ . Note that since $\eta $ is the minimal failure of $\Delta _{0}$ -collection in M,

$$\begin{align*}M\models\exists z\forall\beta<\alpha\exists x\in z\varphi(x,\beta,p). \end{align*}$$

But this is a $\Sigma _{1}$ -statement, so that

$$\begin{align*}M^{\prime}\models\exists z\forall\beta<i(\alpha)\exists x\in z\varphi(x,\beta,i(p)). \end{align*}$$

But then in particular,

$$\begin{align*}M^{\prime}\models\exists x\varphi(x,\alpha^{\prime},i(p)). \end{align*}$$

Contradiction! Therefore, by $\Delta _{0}$ -collection in $M^\prime $ , there is $\beta ^{\prime }<\operatorname {\mathrm {OR}}^{M^{\prime }}$ such that $M^{\prime }\models \forall \alpha <\eta ^{\prime }\exists x\in (M^{\prime }\vert \beta ^{\prime })\varphi (x,\alpha ,i(p)).$ Since i is cofinal, we may assume without loss of generality that $\beta ^{\prime }\in \operatorname {\mathrm {ran}}(i)$ . Let $\beta <\operatorname {\mathrm {OR}}^{M}$ be such that $i(\beta )=\beta ^{\prime }$ . We claim that

$$\begin{align*}M\models\forall\alpha<\eta \exists x\in(M\vert\beta)\varphi(x,\alpha,p), \end{align*}$$

which would be a contradiction! So suppose that there is $\alpha <\eta $ such that

$$\begin{align*}M\models\forall x\in(M\vert\beta)\neg\varphi(x,\alpha,p). \end{align*}$$

This is a $\Delta _0$ statement, so that

$$\begin{align*}M^{\prime}\models\forall x\in(M^{\prime}\vert\beta^{\prime})\neg\varphi(x,\alpha,i(p)). \end{align*}$$

Contradiction!

Now let us suppose that $\theta $ is a limit ordinal. In the case that there is some $\gamma \in b\cap \theta $ such that for all $\xi \in (\gamma ,\theta )\cap b$ , $\deg _\xi ^{\mathcal {T}} \geq 1$ , we can argue as in Case 1 of the successor case. If otherwise we can use the argument from Case 2 of the successor case, since $i_{\gamma \theta }^{\mathcal {T}}$ will be cofinal.

This completes the proof of the lemma.

Proof. We may assume that $\omega \in \text {wfc}(M)$ , as otherwise $\text {wfc}(M) = L_\omega $ which is clearly admissible. It suffices to see that $\text {wfc}(M) \models \Delta _0 \text {-Collection}$ . By induction, it easily follows that for $\alpha < \text {wfo}(M)$ , $S_\alpha ^{\mathbb {E}^M} = (S_\alpha )^M \in \text {wfp}(M)$ , so that $\text {wfc} (M) \subseteq \text {wfp}(M)$ . Let $\varphi $ be a $\Sigma _0$ formula and $a,p \in \text {wfc} (M)$ such that

$$\begin{align*}\text{wfc} (M) \models \forall x \in a \exists y \varphi(x,y,p). \end{align*}$$

Note that by $\Sigma _1$ upwards absoluteness this holds in M. Let $\gamma $ be a non-standard ordinal of M. In $S_\gamma ^M$ , we may define a function F with $\operatorname {\mathrm {dom}}(F) = a$ such that for $x \in a$ ,

$$ \begin{align*} F(x) = \eta \iff S_\gamma^M \models x \in a \land \exists y \in S_{\eta+1} \varphi(x,y,p) \land \forall y \in S_\eta \neg \varphi(x,y,p). \end{align*} $$

Since $\text {wfc} (M) \subseteq S_\gamma ^M$ , it follows by $\Sigma _1$ upwards absoluteness that $F(x) < \text {wfo}(M)$ . However, this means that $\eta := \bigcup _{x \in a} F(x) \subset \text {wfo}(M)$ . Since F is definable over M, we must have that $\eta < \text {wfo}(M)$ . This means that

$$\begin{align*}\text{wfc} (M) \models \forall x \in a \exists y \in S_{\eta} \varphi(x,y,p). \end{align*}$$

Thus, $\text {wfc} (M) \models \text {KP}$ .