# On the consistency of ZF with an elementary embedding from $V_{\lambda+2}$
into $V_{\lambda+2}$

Farmer Schlutzenberg111This is draft version 2 of this document.222 This work
supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation)
under Germany’s Excellence Strategy EXC 2044-390685587, Mathematics Münster:
Dynamics-Geometry-Structure. 333The author thanks Gabriel Goldberg for
bringing Woodin’s questions to his attention, which we discuss here, and other
related questions, and discussions on the topic. We also thank Goldberg for a
key observation which improved the main theorem in an important way (described
below).
<EMAIL_ADDRESS>
###### Abstract

Recall that $I_{0,\lambda}$ is the assertion that $\lambda$ is a limit ordinal
and there is an elementary embedding $j:L(V_{\lambda+1})\to L(V_{\lambda+1})$
with critical point ${<\lambda}$. This hypothesis is usually studied assuming
$\mathsf{ZFC}$ holds in the full universe $V$, but we assume only
$\mathsf{ZF}$.

We show, assuming $\mathsf{ZF}+I_{0,\lambda}$, that there is a proper class
transitive inner model $M$ containing $V_{\lambda+1}$ and modelling the theory

$\mathsf{ZF}+I_{0,\lambda}+\text{``there is an elementary embedding
}j:V_{\lambda+2}\to V_{\lambda+2}\text{''}.$

By employing the results of [9] and [8], we also show that this generalizes to
all even ordinals $\lambda$.

In the case that $\lambda$ is a limit and $\lambda$-$\mathsf{DC}$ holds in
$V$, then the model $M$ constructed also satisfies $\lambda$-$\mathsf{DC}$.

We also show that if $\mathsf{ZFC}+I_{0,\lambda}$ is consistent, then it does
not imply the existence of $V_{\lambda+1}^{\\#}$.

Likewise, if $\mathsf{ZF}+$“$\lambda$ is an even ordinal and
$j:L(V_{\lambda+1})\to L(V_{\lambda+1})$ is elementary with critical point
${<\lambda}$” is consistent, then it does not imply the existence of
$V_{\lambda+1}^{\\#}$. We show that, however, this theory does imply that
$A^{\\#}$ exists for every $A\in V_{\lambda+1}$.

We also make some further observations on $L(V_{\lambda+1})$ under such
hypotheses.

##  1 The Kunen inconsistency

A long standing open question in set theory is whether $\mathsf{ZF}$ suffices
to prove that there is no (non-trivial)444Generally we will omit the phrase
“non-trivial” in this context, where it should obviously be there; sometimes
also “elementary”. elementary embedding

$j:V\to V.$

Such embeddings were introduced by William N. Reinhardt in [13], [14], and the
critical point of such an embedding is now known as a Reinhardt cardinal. A
fundamental theorem is Kunen’s result that such an embedding is inconsistent
with $\mathsf{ZFC}$. His proof involves infinitary combinatorics in
$V_{\lambda+2}$, and he in fact shows under $\mathsf{ZFC}$ that there is no
elementary

$j:V_{\lambda+2}\to V_{\lambda+2}.$

These discoveries led set theorists to ask various natural questions:

  1. –

Does $\mathsf{ZF}$ suffice to prove there is no elementary $j:V\to V$?

  2. –

Does $\mathsf{ZF}$ suffice to prove there is no elementary $j:V_{\lambda+2}\to
V_{\lambda+2}$?

  3. –

Does $\mathsf{ZFC}$ prove there is no elementary $j:V_{\lambda+1}\to
V_{\lambda+1}$?

  4. –

Etc.

However, if a given large cardinal notion is consistent, then of course we
will never know so; the best we can do is to prove relative consistencies, and
to explore the consequences of the large cardinal. Moreover, if $\mathsf{ZF}$
is in fact consistent with $k:V_{\lambda+2}\to V_{\lambda+2}$, this might
suggest that defeating $j:V\to V$ without $\mathsf{AC}$ could demand
significant modifications to Kunen’s $\mathsf{ZFC}$ argument (and other
arguments which have appeared since).

The main aim of this paper is to show that the theory
$\mathsf{ZF}+$“$k:V_{\lambda+2}\to V_{\lambda+2}$ is elementary” is consistent
relative to large cardinals which are traditionally studied in the context of
$\mathsf{ZFC}$.

In §2, we give an overview of the main theorem, and in §3, we state it in
detail and give its proof. In the later sections, we make some further related
observations. In §4, we analyze the existence and uniqueness of extensions of
embeddings related to $I_{0,\lambda}$-embeddings. In §5 we prove some facts on
$\mathrm{HOD}^{L(V_{\lambda+1})}$ and related inner models, assuming
$I_{0,\lambda}$. In §6, we prove that $\mathsf{ZF}+I_{0,\lambda}$ implies that
$A^{\\#}$ exists for every $A\in V_{\lambda+1}$. Most of the results in the
paper hold for arbitrary even ordinals $\lambda$, and $I_{0,\lambda}$ in this
sense, as described in §2.

The papers [3], [6], [5], [1], [2], [17], [16], [9], [8], [20], [10] give
plenty more on large cardinals beyond/without $\mathsf{AC}$. And of course
there is also extensive active research in set theory without $\mathsf{AC}$ in
general.

###  1.1 Notation

Given a structure $N$ and $X\subseteq N$, $\mathrm{Hull}^{N}(X)$ denotes the
set of all $y\in N$ such that $y$ is definable over $N$ from parameters in
$X$, and ${\mathrm{c}\mathrm{Hull}}^{N}(X)$ is the transitive collapse of this
hull, assuming $N$ is transitive and $\mathrm{Hull}^{N}(X)$ is extensional. We
write $\operatorname{Th}^{N}(X)$ for the elementary theory of $N$ in
parameters in $X$.

Given an embedding $j$, we write $\kappa_{0}(j)=\mathrm{crit}(j)$ for the
critical point of $j$, and $\kappa_{\omega}(j)=\sup_{n<\omega}\kappa_{n}$
where $\kappa_{0}=\kappa_{0}(j)$ and $\kappa_{n+1}=j(\kappa_{n})$ (when well
defined).

Regarding ultrapowers, we write $\mathrm{Ult}_{0}(M,\mu)$ for the ultrapower
of structure $M$ mod measure/extender $\mu$, formed using only functions in
$M$ (the “sub-$0$” notation indicates that the functions used are in $M$). In
this context, if $f$ is a function used in forming the ultrapower, then
$[f]^{M,0}_{\mu}$ denotes the element represented by $f$, but normally we
abbreviate this with just $[f]^{M}_{\mu}$ or just $[f]$, if the meaning is
clear. Note that because we do not assume $\mathsf{AC}$, Los’ theorem is not
always immediate for our ultrapowers. We say that the ultrapower “satisfies
Los’ theorem” to mean that the usual statement of Los’ theorem goes through
with respect to this ultrapower (basically that the ultrapower satisfies
$\varphi([f])$ iff $M\models\varphi(f(k))$ for $\mu$-measure one many $k$).
(So this is an abuse of terminology, as otherwise when we write “$U$ satisfies
$\psi$” we mean $U\models\psi$ in the model theoretic sense.)

Let $\lambda$ be a limit ordinal and $X$ a set. A _tree of height
$\leq\lambda$ on $X$_ is a set $\mathscr{T}\subseteq{{}^{<\lambda}X}$ which is
closed under initial segment. That is, each element of $\mathscr{T}$ is a
function $f$ such that $\mathrm{dom}(f)\in\lambda$ and $f:\mathrm{dom}(f)\to
X$, and for each $f\in\mathscr{T}$ and $\beta<\mathrm{dom}(f)$, we have
$f\\!\upharpoonright\\!\beta\in\mathscr{T}$. For $\alpha\leq\lambda$ and
$f:\alpha\to X$, we say that $f$ is a _maximal branch_ of $\mathscr{T}$ iff
either (i) $f\in\mathscr{T}$ but there is no $g\in\mathscr{T}$ with
$\mathrm{dom}(f)<\mathrm{dom}(g)$ and $f\subseteq g$, or (ii) $\alpha$ is a
limit ordinal or $=0$, and $f\\!\upharpoonright\\!\beta\in\mathscr{T}$ for all
$\beta<\alpha$ but $f\notin\mathscr{T}$.

Recall that for $\lambda$ a limit ordinal, $\lambda$-$\mathsf{DC}$ is the
statement that for every set $X$ and every tree $\mathscr{T}$ of height
$\leq\lambda$ on $X$, there is a maximal branch of $\mathscr{T}$.555We remark
that the possibly more standard definition of $\lambda$-$\mathsf{DC}$ is
superficially slightly different; it asserts that for every non-empty set $X$
and every $R\subseteq({{}^{<\lambda}X})\times X$ such that  $\text{ for every
}f\in{{}^{<\lambda}X}\text{ there is some }x\in X\text{ such that }(f,x)\in
R,$ there is $f\in{{}^{\lambda}}X$ such that
$(f\\!\upharpoonright\\!\alpha,f(\alpha))\in R$ for every $\alpha<\lambda$.
The two forms are equivalent modulo $\mathsf{ZF}$ (or less). For given a tree
$\mathscr{T}$ of height $\leq\lambda$ on set $X\neq\emptyset$, define
$R\subseteq({{}^{<\lambda}X})\times X$ by putting $(f,x)\in R$ iff either (i)
$f\ \widehat{\ }\ \left<x\right>\in\mathscr{T}$ or (ii) there is no $y\in X$
such that $f\ \widehat{\ }\ \left<y\right>\in\mathscr{T}$. Clearly $R$
satisfies the requirements for the second form of $\lambda$-$\mathsf{DC}$, and
letting $f:\lambda\to X$ be as there, note that $f\\!\upharpoonright\\!\alpha$
is a maximal branch through $\mathscr{T}$ for some $\alpha\leq\lambda$.
Conversely, let $X,R$ be as in the second form. Let $\mathscr{T}$ be the tree
of all functions $f:\alpha\to X$ where $\alpha<\lambda$ and
$(f\\!\upharpoonright\\!\beta,f(\beta))\in R$ for all $\beta<\alpha$. Let $f$
be a maximal branch through $\mathscr{T}$. Then easily
$\mathrm{dom}(f)=\lambda$, which suffices.666Many authors use the notation
$\mathsf{DC}_{\lambda}$. We use $\lambda$-$\mathsf{DC}$ to distinguish it from
another notion: $\mathsf{DC}_{\mathbb{R}}$ normally denotes the version of
$\omega$-$\mathsf{DC}$ in which the set $X$ is only allowed to be
$\mathbb{R}$.

##  2 $\mathsf{ZF}+j:V_{\lambda+2}\to V_{\lambda+2}$

Recall that the large cardinal axiom $I_{0}$, introduced by Woodin, asserts
that there is a limit ordinal $\lambda$ and an elementary embedding

$j:L(V_{\lambda+1})\to L(V_{\lambda+1})$

with critical point $\mathrm{crit}(j)<\lambda$. We write $I_{0,\lambda}$ to
specify which $\lambda$. This hypothesis sits just below the boundary of where
Kunen’s argument applies. It and strengthenings thereof have been studied by
Woodin, Cramer, Dimonte and others, and an extensive structure theory has been
developed with strong analogues to the Axiom of Determinacy; see [21], [4],
[7]. Many others have also studied other large cardinal notions in this
vicinity. Although $I_{0,\lambda}$ implies that the Axiom of Choice
$\mathsf{AC}$ fails in $L(V_{\lambda+1})$, the hypothesis is usually
considered assuming $\mathsf{ZFC}$ in the background universe $V$. However,
$\mathsf{AC}$ will be mostly unimportant here, and we assume in general only
$\mathsf{ZF}$.

######  Remark 2.1 (Standard extension).

Using the results of [9] or [8], we will prove most of our results for
arbitrary even ordinals $\lambda$, not just limits. This actually makes
virtually no difference to the arguments, and moreover, the reader unfamiliar
with [9] can pretty much just replace every instance of “even” in the paper
with “limit”, without losing much. In §6 the argument differs a little more
between the limit and successor cases, however.

Assume $\mathsf{ZF}$. A standard observation is that if $j:V_{\lambda}\to
V_{\lambda}$ elementary where $\lambda$ is a limit, then there is a unique
possible extension of $j$ to an elementary $j^{+}:V_{\lambda+1}\to
V_{\lambda+1}$; this is defined

$j^{+}(A)=\bigcup_{\alpha<\lambda}j(A\cap V_{\alpha}).$

The key result we need from [9] is that this fact actually generalizes to all
_even_ $\lambda$ (that is, $\lambda=\eta+2n$ for some $n<\omega$): if
$j:V_{\lambda+1}\to V_{\lambda+1}$ is elementary, then $j$ is also the
_canonical extension_ $(j\\!\upharpoonright\\!V_{\lambda})^{+}$ of
$j\\!\upharpoonright\\!V_{\lambda}$, but if $\lambda$ is not a limit, the
definition of the canonical extension is of course not so obvious. Moreover,
$j$ is definable over $V_{\lambda+1}$ from the parameter
$j\\!\upharpoonright\\!V_{\lambda}$, and uniformly so in even ordinals
$\lambda$ and $j$. These facts allow one to lift much of the standard theory
of $I_{0,\lambda}$ to arbitrary even $\lambda$ (a project on which Goldberg
has begun work; this is the topic of [8]).

For most of the paper, the previous paragraph probably suffices as a black box
for the canonical extension, but in §6, the reader will probably need to know
the details of the definition for the successor case to make proper sense.

Note that even in the case that $\lambda$ is a limit, we have a more general
context than standard $I_{0,\lambda}$, because we do not assume $\mathsf{AC}$;
of course, one consequence of that is that $\lambda$ need not be the supremum
of the critical sequence of $j$.777 Recall that under $\mathsf{ZFC}$ in $V$,
$I_{0,\lambda}$ implies $\lambda=\kappa_{\omega}(j)$ is the supremum of the
critical sequence of $j$, where $\kappa_{0}=\mathrm{crit}(j)$ and
$\kappa_{n+1}(j)=j(\kappa_{n}(j))$ and
$\kappa_{\omega}(j)=\sup_{n<\omega}\kappa_{n}(j)$; this yields that $\lambda$
is a strong limit cardinal, $V_{\lambda}$ has a wellorder in $V_{\lambda+1}$,
and $L(V_{\lambda+1})\models\lambda$-$\mathsf{DC}$.

######  Definition 2.2.

Assume $\mathsf{ZF}$ and let $\lambda$ be an even ordinal. An _$I_{0,\lambda}$
-embedding_888This terminology might need to be improved. is an elementary
embedding $j:L(V_{\lambda+1})\to L(V_{\lambda+1})$ with
$\mathrm{crit}(j)<\lambda$ (hence $\mathrm{crit}(j)<\eta$ where $\eta$ is the
largest limit ordinal $\leq\lambda$).

And $I_{0,\lambda}$ is the assertion that there exists an
$I_{0,\lambda}$-embedding.

The main relative consistency result we prove is the following. The author
first proved a slightly weaker result, in which we also assumed that
$V_{\lambda+1}^{\\#}$ exists (but then reached the same conclusion). Goldberg
then observed that the assumption of $V_{\lambda+1}^{\\#}$ could be dispensed
with, by using instead some further calculations of Woodin’s from [21],
establishing the stronger result stated below (likewise for the detailed
version Theorem 3.9). Let us warn the reader in advance that although the
theorem itself seems to be new, the main methods in the proof are in fact old,
and in the most part due to Woodin. (There are a couple of places where one
seems to need to adapt the details of standard kinds of arguments a little,
but as stated, the main methods are well known.)

######  Theorem 2.3.

Let $n<\omega$. If the theory

$\mathsf{ZF}+\text{``there is a limit }\bar{\lambda}\text{ and
}\lambda=\bar{\lambda}+2n\text{ is such that }I_{0,\lambda}\text{''}$

is consistent then so is

$\begin{array}[]{rcl}\mathsf{ZF}&+&\text{``there is a limit
}\bar{\lambda}\text{ and }\lambda=\bar{\lambda}+2n\text{ is such that
}I_{0,\lambda}\\\ &&\text{ and there is an elementary }k:V_{\lambda+2}\to
V_{\lambda+2}\text{''}.\end{array}$

Moreover, just considering limit $\lambda$, if the theory

$\mathsf{ZF}+\text{``there is a limit }\lambda\text{ such that
}\lambda\text{-}\mathsf{DC}+I_{0,\lambda}\text{''}$

is consistent then so is

$\begin{array}[]{rcl}\mathsf{ZF}&+&\text{``there is a limit }\lambda\text{
such that }\lambda\text{-}\mathsf{DC}+I_{0,\lambda}\\\ &&\text{ and there is
an elementary }k:V_{\lambda+2}\to V_{\lambda+2}\text{''}.\end{array}$

We will actually get much more information than this. The models satisfying
“$k:V_{\lambda+2}\to V_{\lambda+2}$ is elementary” will be of the form
$L(V_{\lambda+1},k)$, and satisfy “$V_{\lambda+2}\subseteq L(V_{\lambda+1})$”.

Assume $I_{0,\lambda}$, as witnessed by $j:L(V_{\lambda+1})\to
L(V_{\lambda+1})$. We write throughout $\mathscr{L}=L(V_{\lambda+1})$, so we
have $j:\mathscr{L}\to\mathscr{L}$. Let

$j^{\prime}=j\\!\upharpoonright\\!V_{\lambda+2}^{\mathscr{L}},$

so

$j^{\prime}:V_{\lambda+2}^{\mathscr{L}}\to V_{\lambda+2}^{\mathscr{L}}$

is elementary. Woodin asked in [21, Remark 26], assuming there that
$\mathsf{ZFC}$ holds in $V$ (so $\lambda$ is a limit), whether

$V_{\lambda+2}^{\mathscr{L}(j^{\prime})}\neq V_{\lambda+2}^{\mathscr{L}}$ (1)

must hold. (Here $\mathscr{L}(j^{\prime})=L(V_{\lambda+1},j^{\prime})$. This
is actually just an instance of a more general question he asked.)

The theorem below will show that (1) actually _cannot_ hold (just assuming
$\mathsf{ZF}$ in $V$ and $\lambda$ even); that is, in fact

$V_{\lambda+2}^{\mathscr{L}(j^{\prime})}=V_{\lambda+2}^{\mathscr{L}}$

(though as mentioned above, Woodin’s question was more general, and the
theorem only literally applies to the one case stated here, though of course
there are generalizations). It will follow that

$\mathscr{L}(j^{\prime})\models\mathsf{ZF}+\text{``}j^{\prime}:V_{\lambda+2}\to
V_{\lambda+2}\text{ is elementary''},$

and if $\bar{\lambda}$ is the largest limit ordinal $\leq\lambda$ and
$\bar{\lambda}$-$\mathsf{DC}$ holds in $V$ then we will also get that
$\mathscr{L}(j^{\prime})\models\bar{\lambda}$-$\mathsf{DC}$, giving the main
consistency result.

We will simultaneously address another related question raised by Woodin.
Recall that $V_{\lambda+1}^{\\#}$, if it exists, is the theory of Silver
indiscernibles for $\mathscr{L}=L(V_{\lambda+1})$; its existence is equivalent
to the existence of an elementary $j:\mathscr{L}\to\mathscr{L}$ with
$\mathrm{crit}(j)>\lambda$ (another fact proved by Kunen). Recall the Silver
indiscernibles are a club proper class $\mathscr{I}$ of ordinals, which are
indiscernibles for the model $\mathscr{L}$ with respect to all parameters in
$V_{\lambda+1}$, and such that every element of $\mathscr{L}$ is definable
(equivalently, $\Sigma_{1}$-definable) from finitely many elements of
$\mathscr{I}\cup V_{\lambda+1}$. Note $V_{\lambda+1}^{\\#}$ relates to
$\mathscr{L}$ just as $0^{\\#}$ relates to $L$.999In fact, if one forces over
$V$ by collapsing $V_{\lambda+1}$ to be come countable as usual with finite
conditions, and $G$ is the resulting generic, then $V_{\lambda+1}^{\\#}$ is
almost the same as $x^{\\#}$ where $x$ is a real equivalent to
$(V_{\lambda+1},G)$, and the theory of $x^{\\#}$ is just the relativization of
that of $0^{\\#}$. In particular, $V_{\lambda+1}^{\\#}$ is unique, the
corresponding class $\mathscr{I}$ of Silver indiscernibles is unique,
$V_{\lambda+1}^{\\#}\subseteq V_{\lambda+1}$ (in the codes),
$V_{\lambda+1}^{\\#}\notin\mathscr{L}$, and in fact, $V_{\lambda+1}^{\\#}$
cannot be added by set-forcing to $\mathscr{L}$. Moreover, if $N$ is a proper
class transitive model of $\mathsf{ZF}$ and $V_{\lambda+1}\subseteq N$ and
$N\models$“$V_{\lambda+1}^{\\#}$ exists”, then $V_{\lambda+1}^{\\#}$ exists
and is in $N$ (computed correctly there).

Now Woodin writes in [21, Remark 26] that a “natural conjecture” is that if
$I_{0,\lambda}$ holds, then $V_{\lambda+1}^{\\#}$ exists (under
$\mathsf{ZFC}$, so limit $\lambda$). Note that with the model
$\mathscr{L}(j^{\prime})$ from before, we will have

$\mathscr{L}(j^{\prime})\models\mathsf{ZF}+I_{0,\lambda}+\text{``}V_{\lambda+1}^{\\#}\text{
does not exist''}$

since otherwise $\mathscr{L}(j^{\prime})\models$“$V_{\lambda+1}^{\\#}\in
L(V_{\lambda+1})$”, a contradiction. Now this does not quite disprove the
conjecture just stated, if $\mathsf{ZFC}$ is really the background theory. But
assuming $\mathsf{ZFC}$ in $V$, then there is an easy forcing argument to
reestablish $\mathsf{ZFC}$ in a generic extension of
$L(V_{\lambda+1})[j^{\prime}]$, while preserving $V_{\lambda+1}$, hence
preserving $I_{0,\lambda}$, thus obtaining a failure of the
$V_{\lambda+1}^{\\#}$ conjecture.

######  Definition 2.4.

Let $j:\mathscr{L}\to\mathscr{L}$ with $\mathrm{crit}(j)<\lambda$. Equivalent
to the terminology of [21] in this case, we say that $j$ is _proper_ iff
either (i) $V_{\lambda+1}^{\\#}$ does not exist, or (ii) $V_{\lambda+1}^{\\#}$
exists and $j\\!\upharpoonright\\!\mathscr{I}^{\mathscr{L}}=\mathrm{id}$.

We now describe the main point of the construction. Let us assume for the
purposes of this sketch that $V_{\lambda+1}^{\\#}$ exists, and let
$\mathscr{I}^{\mathscr{L}}$ denote the class of Silver indiscernibles for
$\mathscr{L}$. Let $j:\mathscr{L}\to\mathscr{L}$ witness $I_{0,\lambda}$. By
Proposition 3.3 below, we may assume that $j$ is proper (that is,
$j\\!\upharpoonright\\!\mathscr{I}^{\mathscr{L}}=\mathrm{id}$). We will show
later that $j$ is iterable (this will be defined in 3.7 below, but it is
analogous to linearly iterating $V$ with a measure). Let
$\left<\mathscr{L}_{n},j_{n}\right>_{n\leq\omega}$ be the length $(\omega+1)$
iteration of $(\mathscr{L}_{0},j_{0})=(\mathscr{L},j)$ (so
$\mathscr{L}_{n}=\mathscr{L}$ for each $n<\omega$, but $\mathscr{L}_{\omega}$
is the direct limit). Let $j_{0\omega}:\mathscr{L}_{0}\to\mathscr{L}_{\omega}$
be the resulting direct limit map. Let
$k_{0\omega}=j_{0\omega}\\!\upharpoonright\\!V_{\lambda+2}^{\mathscr{L}}$. Now
the key point is that there is a strong analogy between the models

$\mathscr{L}[k_{0\omega}]\text{ and }M_{1}[\Sigma],$

where $M_{1}$ is the minimal iterable proper class fine structural mouse with
1 Woodin cardinal and $\Sigma$ an appropriate fragment of its iteration
strategy. Actually aside from some small extra details with Los’ theorem
without full $\mathsf{AC}$ (which however are as in [21]), and the necessity
of proving iterability, things are simpler here than for $M_{1}[\Sigma]$. The
main calculations are so analogous, that the reader familiar with Woodin’s
analysis of $M_{1}[\Sigma]$ (see [11]) and possibly some of Woodin’s arguments
in [21] and/or the analysis of Silver indiscernibles in [18] or [15], may now
wish to use the hint just mentioned and try working through the proof
independently, at least assuming the iterability just mentioned, and maybe
that $V_{\lambda+1}^{\\#}$ exists.

There are, however, a couple of points where some details of the
implementation are not quite standard, as far as the author is aware. One is
that the proof of iterability we will give combines two techniques in a way
that might be new, although this is anyway unnecessary in the case that
$\mathsf{ZFC}$ holds in $V$, by Woodin’s iterability results under
$\mathsf{ZFC}$.101010 See [21, Lemma 21]; the proof seems to make at least
some use of $\mathsf{DC}$. We haven’t tried to adapt the methods there
directly; we give a somewhat different proof of iterability here. Another is
that in the $M_{1}[\Sigma]$ context, towards the end of the calculation, one
forms the hull
$H=\mathrm{Hull}^{M_{\infty}[\Lambda]}(\mathrm{rg}(i_{M_{1}\infty}))$ and
shows that $H\cap M_{\infty}=\mathrm{rg}(i_{M_{1}\infty})$, and hence that
$M_{1}[\Sigma]$ is the transitive collapse. In the mouse case, it is immediate
that $H\preccurlyeq M_{\infty}[\Lambda]$. But in our case the analogue seems
to require a little more thought.

And of course, a formally new feature is that $\lambda$ is allowed be an
arbitrary even ordinal (and we only assume $\mathsf{ZF}$). But modulo [9] (see
Remark 2.1), the argument in the even successor case is virtually identical to
the limit case.

##  3 The main argument

We first state some definitions and facts about the existence and uniqueness
of extensions of embeddings to $I_{0,\lambda}$-embeddings, which are relevant
to the models we construct in the main proof; these things are basically as in
[21] (although recall we only assume $\mathsf{ZF}$), and also see [9] for more
on the measure defined below:

######  Definition 3.1.

Assume $\mathsf{ZF}$ and let $\lambda$ be even. Let
$j:\mathscr{L}\to\mathscr{L}$ with $\mathrm{crit}(j)<\lambda$. Then $\mu_{j}$
denotes the measure on $V_{\lambda+1}$ derived from $j$ with seed
$j\\!\upharpoonright\\!V_{\lambda}$:

$\mu_{j}=\\{X\in\mathcal{P}(V_{\lambda+1})\cap\mathscr{L}\bigm{|}j\\!\upharpoonright\\!V_{\lambda}\in
j(X)\\}.$

The ultrapower $\mathrm{Ult}_{0}(\mathscr{L},\mu_{j})$ (with the “sub-$0$”
notation)111111The notation is meaningful in fine structure theory, where it
corresponds to $\Sigma_{0}$. denotes that constructed using only functions
$f\in\mathscr{L}$ such that $f:V_{\lambda+1}\to\mathscr{L}$. We write
$[f]^{\mathscr{L}}_{\mu_{j}}$, or just $[f]$, for the element of the
ultrapower represented by $f$. Given such functions $f,g$, we write
$f=_{\mu_{j}}g$ iff

$\\{k\in V_{\lambda+1}\bigm{|}f(k)=g(k)\\}\in\mu_{j},$

and similarly for $f\in_{\mu_{j}}g$.

We say that $\mu_{j}$ is _weakly amenable_ to $\mathscr{L}$ iff for each
$\pi:V_{\lambda+1}\to V_{\lambda+2}^{\mathscr{L}}$ with $\pi\in\mathscr{L}$,
we have $\mathrm{rg}(\pi)\cap\mu_{j}\in\mathscr{L}$.

######  Definition 3.2.

Given a transitive set $X$, $\Theta_{X}$ denotes the supremum of all ordinals
$\alpha$ such that $\alpha$ is the surjective image of $X$. When we write just
$\Theta$, we mean $\Theta_{V_{\lambda+1}}^{\mathscr{L}}$.

The following lemma is just a direct shift of calculations of Woodin from [21]
over to the $\mathsf{ZF}+$even context (using [9]):

######  Proposition 3.3 (Woodin).

Assume $\mathsf{ZF}$ and let $\lambda$ be even and
$j:\mathscr{L}\to\mathscr{L}$ be elementary with $\mathrm{crit}(j)<\lambda$.
Let $U=\mathrm{Ult}_{0}(\mathscr{L},\mu_{j})$ and $j_{0}:\mathscr{L}\to U$ be
the ultrapower map. Then:

  1. 1.

$\mu_{j}$ is weakly amenable to $\mathscr{L}$,

  2. 2.

$U$ is extensional and isomorphic to $\mathscr{L}$; we take $U=\mathscr{L}$,

  3. 3.

$j_{0}:\mathscr{L}\to U=\mathscr{L}$ is elementary,

  4. 4.

$j_{0}\\!\upharpoonright\\!L_{\Theta}(V_{\lambda+1})=j\\!\upharpoonright\\!L_{\Theta}(V_{\lambda+1})$
where $\Theta=\Theta_{V_{\lambda+1}}^{\mathscr{L}}$,

  5. 5.

if $V_{\lambda+1}^{\\#}$ does not exist then $j_{0}=j$ is proper and
$[f]^{\mathscr{L}}_{\mu}=j(f)(j\\!\upharpoonright\\!V_{\lambda})$.

Now suppose further that $V_{\lambda+1}^{\\#}$ exists. Then:

  1. 6.

$j_{0}\\!\upharpoonright\\!\mathscr{I}^{\mathscr{L}}=\mathrm{id}$, so $j_{0}$
is proper,

  2. 7.

$j``\mathscr{I}^{\mathscr{L}}\subseteq\mathscr{I}^{\mathscr{L}}$,

and letting $j_{1}:\mathscr{L}\to\mathscr{L}$ be the unique elementary map
with $\mathrm{crit}(j_{1})\geq\min(\mathscr{I}^{\mathscr{L}})$ and
$j_{1}\\!\upharpoonright\\!\mathscr{I}^{\mathscr{L}}\subseteq j$, we have

  1. 8.

$j_{1}\circ j_{0}=j$ and
$j_{1}([f]^{\mathscr{L}}_{\mu_{j}})=j(f)(j\\!\upharpoonright\\!V_{\lambda})$.

Moreover (still assuming $V_{\lambda+1}^{\\#}$ exists) this is the unique pair
$(j^{\prime}_{0},j^{\prime}_{1})$ such that
$j^{\prime}_{i}:\mathscr{L}\to\mathscr{L}$ is elementary for $i=0,1$,
$j=j^{\prime}_{1}\circ j^{\prime}_{0}$, $j^{\prime}_{0}$ is proper and
$\mathrm{crit}(j^{\prime}_{1})\geq\lambda$.

###### Proof.

First consider weak amenability. Let $\pi\in\mathscr{L}$ with
$\pi:V_{\lambda+1}\to V_{\lambda+2}^{\mathscr{L}}$. Then
$j(\pi):V_{\lambda+1}\to V_{\lambda+2}^{\mathscr{L}}$, and since
$j\\!\upharpoonright\\!V_{\lambda}\in V_{\lambda+1}$, by Remark 2.1, we have
$k=j\\!\upharpoonright\\!V_{\lambda+1}\in L(V_{\lambda+1})$. But then note
that for $x\in V_{\lambda+1}$, we have

$\pi(x)\in\mu_{j}\iff j\\!\upharpoonright\\!V_{\lambda}\in j(\pi)(j(x))\iff
j\\!\upharpoonright\\!V_{\lambda}\in j(\pi)(k(x)),$

and since $j(\pi),k\in L(V_{\lambda+1})$, therefore
$\mathrm{rg}(\pi)\cap\mu_{j}\in L(V_{\lambda+1})$, as desired.

Now write
$\mathscr{F}=\\{f\in\mathscr{L}\bigm{|}f:V_{\lambda+1}\to\mathscr{L}\\}$, the
class of functions used to form $U$. Let

$U^{\prime}=\\{j(f)(j\\!\upharpoonright\\!V_{\lambda})\bigm{|}f\in\mathscr{F}\\}$

and

$H=\mathrm{Hull}^{\mathscr{L}}(\mathrm{rg}(j)\cup\\{j\\!\upharpoonright\\!V_{\lambda}\\}).$

Then $U\cong U^{\prime}=H$. For $U\cong U^{\prime}$ directly from the
definition. But clearly $U^{\prime}\subseteq H$, and if $a,x\in\mathscr{L}$
and $\varphi$ is a formula and

$x=\text{ the unique }x^{\prime}\in\mathscr{L}\text{ such that
}\mathscr{L}\models\varphi(x^{\prime},j(a),j\\!\upharpoonright\\!V_{\lambda})$

then let $f:V_{\lambda+1}\to\mathscr{L}$ be the function

$f(k)=\text{ the unique }x^{\prime}\text{ such that
}\mathscr{L}\models\varphi(x^{\prime},a,k),$

if a unique such $x^{\prime}$ exists, and $f(k)=\emptyset$ otherwise. Then
$j(f)(j\\!\upharpoonright\\!V_{\lambda})=x\in U^{\prime}$, as desired.

Now $V_{\lambda+1}\subseteq H$, because given any $y\in V_{\lambda+1}$, we
have

$y=(j\\!\upharpoonright\\!V_{\lambda})^{-1}``j(y).$

Since $\mathscr{L}\models$“$V=\mathrm{HOD}(V_{\lambda+1})$”, it follows that
$H\preccurlyeq\mathscr{L}$.

Now since $U\cong U^{\prime}=H\preccurlyeq\mathscr{L}$, $U$ is extensional and
wellfounded, so we identify it with its transitive collapse. Let
$j_{0}:\mathscr{L}\to U$ be the ultrapower map, and $j_{1}:U\to\mathscr{L}$ be
the natural factor map

$j_{1}([f])=j(f)(j\\!\upharpoonright\\!V_{\lambda}).$

Note then that $U$ is just the transitive collapse of $H$, which is just
$\mathscr{L}$, and $j_{1}$ is the uncollapse map. Since
$H\preccurlyeq\mathscr{L}$, $j_{1}$ is elementary and if
$j_{1}\neq\mathrm{id}$ then $\mathrm{crit}(j_{1})>\lambda$, in which case
$V_{\lambda+1}^{\\#}$ exists and
$\mathrm{crit}(j_{1})\geq\min(\mathscr{I}^{\mathscr{L}})$ and $j_{1}$ is
determined by its action on $\mathscr{I}^{\mathscr{L}}$. Note that
$j=j_{1}\circ j_{0}$. So $j_{0}=j_{1}^{-1}\circ j$ is elementary with
$j_{0}\\!\upharpoonright\\!V_{\lambda}=j\\!\upharpoonright\\!V_{\lambda}$, and
if $j_{1}\neq\mathrm{id}$ (so $V_{\lambda+1}^{\\#}$ exists) then
$j_{0}\\!\upharpoonright\\!\mathscr{I}^{\mathscr{L}}=\mathrm{id}$, because
$j_{0}$ is an ultrapower map, via functions in $\mathscr{L}$.

The rest is clear. ∎

######  Definition 3.4.

Under the assumptions of the previous lemma, the factoring $j=j_{1}\circ
j_{0}$ is the _standard decomposition_ of $j$, where if $V_{\lambda+1}^{\\#}$
does not exist then $j=j_{0}$ and $j_{1}=\mathrm{id}$.

######  Definition 3.5.

Suppose $V_{\lambda+1}^{\\#}$ exists. Let $0<n<\omega$ and
$s\in[\mathscr{I}^{\mathscr{L}}]^{<\omega}$ with $\operatorname{card}(s)=n$.
Write $s^{-}=s\backslash\\{\max(s)\\}$. For $\alpha\in\mathrm{OR}$ with
$\alpha>\lambda+1$ write $\mathscr{L}|\alpha=L_{\alpha}(V_{\lambda+1})$.
Define the theory

$t_{n}=\operatorname{Th}^{\mathscr{L}|\max(s)}(V_{\lambda+1}\cup\\{s^{-}\\}),$

coded as a subset of $V_{\lambda+1}$. (Here $\operatorname{Th}^{N}(X)$ denotes
the elementary theory of the structure $N$ in parameters in $X$.) Define the
ordinal

$\bar{\iota}_{n}=\mathrm{OR}({\mathrm{c}\mathrm{Hull}}^{\mathscr{L}|\max(s)}(V_{\lambda+1}\cup\\{s^{-}\\})),$

(see §1.1 for notation).

######  Proposition 3.6.

Assume $\mathsf{ZF}$ and let $\lambda$ be even. Then:

  1. 1.

Every elementary $\ell:V_{\lambda}\to V_{\lambda}$ extends to at most one
proper $I_{0,\lambda}$-embedding.

  2. 2.

Suppose $V_{\lambda+1}^{\\#}$ exists. Then:

    1. –

Let $k:V_{\lambda+2}^{\mathscr{L}}\to V_{\lambda+2}^{\mathscr{L}}$ be
$\Sigma_{1}$-elementary. Then $k$ extends to an $I_{0,\lambda}$-embedding iff
$k(t_{n})=t_{n}$ for each $n<\omega$.

    2. –

Let $k:L_{\Theta}(V_{\lambda+1})\to L_{\Theta}(V_{\lambda+1})$ be
$\Sigma_{1}$-elementary. Then $k$ extends to an $I_{0,\lambda}$-embedding iff
$k(t_{n})=t_{n}$ for each $n<\omega$ iff $k(\bar{\iota}_{n})=\bar{\iota}_{n}$
for each $n<\omega$.

###### Proof.

Part 1: First, the canonical extension $\ell^{+}$ is the unique possible
elementary extension of $\ell$ to a map $V_{\lambda+1}\to V_{\lambda+1}$; see
2.1. So if $V_{\lambda+1}^{\\#}$ exists then since
$\mathscr{L}=\mathrm{Hull}^{\mathscr{L}}(\mathscr{I}^{\mathscr{L}}\cup
V_{\lambda+1})$, the uniqueness of a proper extension of $\ell$ is clear.
Suppose $V_{\lambda+1}^{\\#}$ does not exist, and $\ell_{0},\ell_{1}$ are two
proper extensions of $\ell$, hence extending $\ell^{+}$. Then by Proposition
3.3, $\ell_{0},\ell_{1}$ are the ultrapower maps with respect to
$\mu_{\ell_{0}},\mu_{\ell_{1}}$. Therefore we can find a proper class $\Gamma$
of common fixed points for $\ell_{0},\ell_{1}$. Since
$\ell_{0}\\!\upharpoonright\\!V_{\lambda+1}=\ell^{+}=\ell_{1}\\!\upharpoonright\\!V_{\lambda+1}$,
therefore $\ell_{0}\\!\upharpoonright\\!H=\ell_{1}\\!\upharpoonright\\!H$
where

$H=\mathrm{Hull}^{\mathscr{L}}(\Gamma\cup V_{\lambda+1}).$

So it suffices to see $\mathscr{L}=H$. Suppose not. Then
$H\preccurlyeq\mathscr{L}$ as before. We get that $\mathscr{L}$ is the
transitive collapse of $H$ and letting $k:\mathscr{L}\to\mathscr{L}$ be the
uncollapse map, then $\mathrm{crit}(k)>\lambda$. But then
$V_{\lambda+1}^{\\#}$ exists, contradiction.

Part 2: This is basically routine; the fact that if $k$ extends to an
$I_{0,\lambda}$-embedding then $k(\bar{\iota}_{n})=\bar{\iota}_{n}$, is
because $\bar{\iota}_{n}$ is definable over $\mathscr{L}$ from $s$ and
$\lambda$, where $s\in[\mathscr{I}^{\mathscr{L}}]^{n}$. ∎

We now define iterability, following [21]:

######  Definition 3.7.

Let $\lambda$ be a even and $j$ a proper $I_{0,\lambda}$-embedding. We define
the $\alpha$th iterate
$(\mathscr{L}_{\alpha},\lambda_{\alpha},j_{\alpha},\mu_{\alpha})$ of
$(\mathscr{L},\lambda,j,\mu_{j})$. We set $\mathscr{L}_{0}=\mathscr{L}$ and
$\lambda_{0}=\lambda$ and $j_{0}=j$ and $\mu_{0}=\mu_{j}$. Given
$(\mathscr{L}_{\alpha},\lambda_{\alpha},j_{\alpha},\mu_{\alpha})$, set
$\mathscr{L}_{\alpha+1}=\mathscr{L}_{\alpha}$ and
$\lambda_{\alpha+1}=\lambda_{\alpha}$ and letting

$\mu_{\alpha}^{-}=\\{\mathrm{rg}(\pi)\cap\mu_{\alpha}\bigm{|}\pi\in\mathscr{L}_{\alpha}\text{
and }\pi:V_{\lambda_{\alpha}+1}\to
V_{\lambda_{\alpha}+2}^{\mathscr{L}_{\alpha}}\\},$

set

$\mu_{\alpha+1}=\bigcup_{X\in\mu_{\alpha}^{-}}j_{\alpha}(X).$

Noting that $\mu_{\alpha+1}$ is an $\mathscr{L}_{\alpha+1}$-ultrafilter, if
$\mathrm{Ult}(\mathscr{L}_{\alpha+1},\mu_{\alpha+1})$ satisfies Los’ theorem,
and is wellfounded and $=\mathscr{L}_{\alpha+1}$, we set $j_{\alpha+1}$ to be
the ultrapower map, and otherwise stop the construction. At limit stages
$\eta$ we take direct limits to define
$\mathscr{L}_{\eta},\lambda_{\eta},U_{\eta}$, and then attempt to define
$j_{\eta}$ as before.

We say that $(\mathscr{L},j)$ is _$\eta$ -iterable_ iff $\mathscr{L}_{\alpha}$
is defined (and wellfounded) for all $\alpha<\eta$. We say that
$(\mathscr{L},j)$ is _iterable_ iff $\eta$-iterable for all
$\eta\in\mathrm{OR}$.

If $N\models\mathsf{ZF}$ is a transitive class with
$\mathscr{L}=L(V_{\lambda+1})^{N}$ and
$V_{\lambda+2}^{\mathscr{L}}=V_{\lambda+2}^{N}$ and $\mu_{j}\in N$, then the
iterates of $N$ with respect to $\mu_{j}$ are just defined internally to $N$
(just like iterating $V$ with respect to a measure under $\mathsf{ZFC}$). In
this case, we say that $N$ is a _tight extension_ of $\mathscr{L}$ if for
every function $f\in N$ with $f:V_{\lambda+1}\to\mathscr{L}$ there is
$g\in\mathscr{L}$ such that $f=_{\mu_{j}}g$.

######  Lemma 3.8.

Adopt notation as above, and suppose that $N$ is a tight extension of
$\mathscr{L}$. Suppose that the ultrapower $\mathrm{Ult}_{0}(N,\mu_{j})$
satisfies Los’ theorem. Then $\mu_{j}$ is iterable, both in the sense of
iterating $\mathscr{L}$ as above, or $N$ internally as above. Moreover, let
$\left<\mathscr{L}_{\alpha},\lambda_{\alpha},\mu_{\alpha},j_{\alpha}\right>_{\alpha\in\mathrm{OR}}$
be the iterates of $(\mathscr{L},\mu_{j})$ and
$j_{\alpha\beta}:\mathscr{L}_{\alpha}\to\mathscr{L}_{\beta}$ the iteration
maps, and
$\left<N_{\alpha},\mu^{\prime}_{\alpha}\right>_{\alpha\in\mathrm{OR}}$ be the
(internal) iterates of $(N,\mu_{j})$ and $j^{\prime}_{\alpha\beta}$ the
iteration maps. Then $\mathscr{L}_{\alpha}=j^{\prime}_{0\alpha}(\mathscr{L})$
and $\mu_{\alpha}=\mu^{\prime}_{\alpha}$ and $j_{\alpha\beta}\subseteq
j^{\prime}_{\alpha\beta}$, and the iteration maps are elementary.

###### Proof.

We already know that $\mathrm{Ult}_{0}(\mathscr{L},\mu_{j})$ is wellfounded
and isomorphic to $\mathscr{L}$, by 3.3. By Los’ theorem, the ultrapower
$\mathrm{Ult}_{0}(N,\mu_{j})$ is extensional and the ultrapower map
$i^{N}_{\mu_{j}}$ is elementary. And because $N$ is a tight extension, Because
$N$ is a tight extension, note that $\mathrm{Ult}_{0}(N,\mu_{j})$ is
wellfounded and

$L(V_{\lambda+1})^{\mathrm{Ult}_{0}(N,\mu_{j})}=i^{N}_{\mu_{j}}(\mathscr{L})=\mathrm{Ult}_{0}(\mathscr{L},\mu_{j})=\mathscr{L}$

and

$i^{N}_{\mu_{j}}\\!\upharpoonright\\!\mathscr{L}=i^{\mathscr{L}}_{\mu_{j}}.$

It is easy enough to see that also $\mu_{1}=\mu^{\prime}_{1}$. By this and by
the elementarity of all of the assumed facts hold also for
$\mathscr{L}_{1},j_{1},\mu_{1}=\mu^{\prime}_{1},N_{1}$, and note that in this
way we also get Los’ theorem and extensionality for
$\mathrm{Ult}_{0}(\mathscr{L}_{1},\mu_{1})$. Therefore we can iterate the
process, and the same facts and relationships hold for the iterates, assuming
wellfoundedness. But then the usual proof of linear iterability shows that all
iterates of $(N,\mu_{j})$ are wellfounded, and hence so are the
$\mathscr{L}_{\alpha}$. ∎

We can now state the main theorem of the paper.

######  Theorem 3.9.

Assume $\mathsf{ZF}+I_{0,\lambda}$ where $\lambda$ is even. Write
$\mathscr{L}=L(V_{\lambda+1})$. Let $j:\mathscr{L}\to\mathscr{L}$ be
elementary with $\mathrm{crit}(j)<\lambda$. Let $j=j_{1}\circ j_{0}$ be the
standard decomposition of $j$. Let
$j^{-}=j\\!\upharpoonright\\!V_{\lambda+2}^{\mathscr{L}}$, so $j^{-}\subseteq
V_{\lambda+2}^{\mathscr{L}}$. Write
$\mathscr{L}[j^{-}]=L(V_{\lambda+1},j^{-})$. Then:

  1. 1.

$V_{\lambda+2}^{\mathscr{L}}=V_{\lambda+2}^{\mathscr{L}[j^{-}]}$,

  2. 2.

$\mathscr{L}[j^{-}]\models\mathsf{ZF}$, $j_{0}$ is definable over
$\mathscr{L}[j^{-}]$ from $j^{-}$, and $\mathscr{L}[j^{-}]$ satisfies the
following statements:

    1. (a)

$j^{-}:V_{\lambda+2}\to V_{\lambda+2}$ is elementary,

    2. (b)

$I_{0,\lambda}$ holds, as witnessed by $j_{0}$, which is also proper and
extends $j^{-}$,

    3. (c)

$V_{\lambda+2}\subseteq\mathscr{L}=L(V_{\lambda+1})$, so $V_{\lambda+1}^{\\#}$
does not exist,

    4. (d)

$\Theta_{V_{\lambda+1}}^{\mathscr{L}}=\Theta_{V_{\lambda+1}}$ is regular.

  3. 3.

$\mu_{j}$ is iterable, with respect to iterating either $\mathscr{L}$ as in
Definition 3.7121212 Note that in [21], Woodin proves iterability assuming
$\mathsf{ZFC}$ in $V$. or $\mathscr{L}[j^{-}]$ internally. Moreover,
$\mathscr{L}[j^{-}]$ is a tight extension of $\mathscr{L}$.

  4. 4.

If $\eta\leq\lambda$, $\eta$ is a limit and $V\models\eta$-$\mathsf{DC}$ then
$\mathscr{L}\models\eta$-$\mathsf{DC}$ and
$\mathscr{L}[j^{-}]\models\eta$-$\mathsf{DC}$.

######  Definition 3.10.

Given $n<\omega$, write $I_{0,\lambda,2n}$ for the assertion “there is a limit
ordinal $\bar{\lambda}$ such that $\lambda=\bar{\lambda}+2n$ and
$I_{0,\lambda}$”.

######  Corollary 3.11.

We have:

  1. 1.

For each $n<\omega$, if $\mathsf{ZF}+\exists\lambda[I_{0,\lambda,2n}]$ is
consistent then so is

$\mathsf{ZF}+\exists\lambda[I_{0,\lambda,2n}+\text{``}V_{\lambda+2}\subseteq
L(V_{\lambda+1})\text{''}+\text{``there is an elementary }k:V_{\lambda+2}\to
V_{\lambda+2}]\text{''.}$

  2. 2.

$\mathrm{Con}(\mathsf{ZF}+\lambda\text{ a limit
}+\lambda\text{-}\mathsf{DC}+I_{0,\lambda})\implies\mathrm{Con}(\mathsf{ZF}+\lambda\text{
a limit }+\lambda\text{-}\mathsf{DC}+I_{0,\lambda}+$“$V_{\lambda+2}\subseteq
L(V_{\lambda+1})$”$+$“there is an elementary $k:V_{\lambda+2}\to
V_{\lambda+2}$”$)$.

  3. 3.

$\mathrm{Con}(\mathsf{ZFC}+\lambda\text{ a limit
}+I_{0,\lambda})\implies\mathrm{Con}(\mathsf{ZFC}+\lambda\text{ a limit
}+I_{0,\lambda}+$“ $V_{\lambda+1}^{\\#}$ does not exist”$)$.

  4. 4.

Assume $\mathsf{ZF}+\lambda$-$\mathsf{DC}$ where $\lambda$ is a limit,
$V_{\lambda+1}^{\\#}$ exists and there is an elementary131313 Clearly if
$j:L(V_{\lambda+1},V_{\lambda+1}^{\\#})\to
L(V_{\lambda+1},V_{\lambda+1}^{\\#})$ is elementary with
$\mathrm{crit}(j)<\lambda$, then
$k=j\\!\upharpoonright\\!L_{\omega}(V_{\lambda+1})$ is such an embedding. Also
$j:V_{\lambda+2}\to V_{\lambda+2}$ is $\Sigma_{1}$-elementary and
$V_{\lambda+1}^{\\#}$ exists then $j(V_{\lambda+1}^{\\#})=V_{\lambda+1}^{\\#}$
and $j$ induces a $k$ as hypothesized.

$k:L_{\omega}(V_{\lambda+1},V_{\lambda+1}^{\\#})\to
L_{\omega}(V_{\lambda+1},V_{\lambda+1}^{\\#}).$

Then there is a limit $\bar{\lambda}<\lambda$ such that $I_{0,\bar{\lambda}}$
holds, and there is a proper class inner model $N$ such that:

    1. –

$V_{\bar{\lambda}+1}\subseteq N$ and
$V_{\bar{\lambda}+2}^{N}=V_{\bar{\lambda}+2}\cap L(V_{\bar{\lambda}+1})$,

    2. –

$N\models\mathsf{ZF}+\bar{\lambda}$-$\mathsf{DC}+I_{0,\bar{\lambda}}$,

    3. –

$N\models$“there is an elementary $\bar{k}:V_{\bar{\lambda}+2}\to
V_{\bar{\lambda}+2}$”.

###### Proof.

Parts 1,2 are directly by the theorem.

Part 3: Assume $\mathsf{ZFC}+I_{0,\lambda}$ (so $\lambda$ is a limit) and let
$j,j_{0}$ etc be as in the theorem. So $\lambda$ is a limit of measurables and
$\operatorname{cof}(\lambda)=\omega$, so there is a wellorder of $V_{\lambda}$
in $V_{\lambda+1}$, and $\lambda^{+}$ is regular. Let $\mathbb{P}$ be the
forcing for adding a surjection $f:\lambda^{+}\to V_{\lambda+1}$, with
conditions functions $p:\alpha\to V_{\lambda+1}$ for some
$\alpha<\lambda^{+}$. So
$\mathbb{P}\in\mathscr{L}\subseteq\mathscr{L}[j^{-}]$, and $\mathbb{P}$ is
$\lambda$-closed. Let $G$ be $(V,\mathbb{P})$-generic. Then note that

$V_{\lambda+1}^{V[G]}=V_{\lambda+1}=V_{\lambda+1}^{\mathscr{L}[j^{-}][G]}.$

Note then that
$\mathscr{L}[j^{-}][G]\models\mathsf{ZFC}+I_{0,\lambda}+\text{``}V_{\lambda+1}^{\\#}\text{
does not exist}\text{''}$.

Part 4: We use the following theorem of Cramer (see [4, Theorem 3.9]):

######  Fact 3.12 (Cramer).

Assume $\mathsf{ZFC}$, $\lambda$ is a limit and $V_{\lambda+1}^{\\#}$ exists.
Suppose there is an elementary

$k^{\prime}:L_{\omega}(V_{\lambda+1},V_{\lambda+1}^{\\#})\to
L_{\omega}(V_{\lambda+1},V_{\lambda+1}^{\\#}).$

Then $I_{0,\bar{\lambda}}$ holds at some $\bar{\lambda}<\lambda$.

Now with $k^{\prime}=k$, we have everything required to apply Cramer’s
theorem, except that we only have $\lambda$-$\mathsf{DC}$, not full
$\mathsf{AC}$. But note we may assume $\lambda=\kappa_{\omega}(k)$. So
$\lambda$ is a strong limit cardinal, $V_{\lambda}\models\mathsf{ZFC}$, and
$\lambda^{+}$ is regular. Let $\mathbb{P},G$ be as before, and now work in
$M=L(V_{\lambda+1},V_{\lambda+1}^{\\#},k^{\prime},G)$. Note that
$M\models\mathsf{ZFC}$, so we can apply Fact 3.12 in $M$.

So fix $\bar{\lambda}<\lambda$ such that in $M\models I_{0,\bar{\lambda}}$, as
witnessed by $\bar{j}$, with $\bar{j}$ proper. Then by Theorem 3.9,
$N=L(V_{\bar{\lambda+1}})[\bar{j}]$ has the right properties, and because
$V_{\lambda+1}^{M}=V_{\lambda+1}^{V}$, and $\bar{j}$ is determined by
$\mu_{\bar{j}}$, we actually have $N\subseteq V$, so we are done. ∎

We now proceed to the main argument.

###### Proof of Theorem 3.9.

We begin with a couple of claims, with calculations essentially as in [21]. We
will also need the details of their proofs later for the main argument. Assume
$I_{0,\lambda}$, and let $j:\mathscr{L}\to\mathscr{L}$ be a proper
$I_{0,\lambda}$-embedding. Fix a proper class
$\Gamma\subseteq\mathrm{OR}\backslash(\lambda+1)$ such that
$j\\!\upharpoonright\\!\Gamma=\mathrm{id}$, taking
$\Gamma=\mathscr{I}^{\mathscr{L}}$ if $V_{\lambda+1}^{\\#}$ exists. Let
$\vec{\Gamma}=[\Gamma]^{<\omega}\backslash\\{\emptyset\\}$. For
$s\in\vec{\Gamma}$ let $s^{-}=s\backslash\\{\max(s)\\}$, and let

$H^{s}=\mathrm{Hull}^{\mathscr{L}|\max(s)}(V_{\lambda+1}\cup\\{s^{-}\\}).$

Note this is the uncollapsed hull and $H^{s}\preccurlyeq\mathscr{L}|\max(s)$,
because

$\mathscr{L}|\max(s)=\mathrm{Hull}^{\mathscr{L}|\max(s)}(V_{\lambda+1}\cup\max(s)).$

Given any elementary $k:\mathscr{L}\to\mathscr{L}$ such that
$k\\!\upharpoonright\\!\Gamma=\mathrm{id}$, let

$k^{s}=k\\!\upharpoonright\\!H^{s}:H^{s}\to H^{s}.$

Note that $k^{s}$ is the unique elementary map $\pi:H^{s}\to H^{s}$ such that
$k\\!\upharpoonright\\!V_{\lambda}\subseteq\pi$ and $\pi(s^{-})=s^{-}$ (since
$k\\!\upharpoonright\\!V_{\lambda+1}$ must be the canonical extension of
$k\\!\upharpoonright\\!V_{\lambda}$). Therefore $k^{s}\in\mathscr{L}$.

######  Claim 1.

Let $\mu_{0}=\mu_{j}$ and $\mu_{1}$ be as in Definition 3.7, and
$j_{01}=j=i^{\mathscr{L}}_{\mu_{0}}$ and $j_{12}=i^{\mathscr{L}}_{\mu_{1}}$
(the ultrapower maps; we haven’t shown yet that
$\mathrm{Ult}(\mathscr{L},\mu_{1})$ is wellfounded etc).141414 Notationally
$j_{mn}:\mathscr{L}_{m}\to\mathscr{L}_{n}$. Then:

  1. 1.

$j_{01}\\!\upharpoonright\\!(\mathscr{L}|\alpha)\in\mathscr{L}$ for each
$\alpha<\Theta=\Theta_{V_{\lambda+1}}^{\mathscr{L}}$,

and letting
$k=\bigcup_{\alpha<\Theta}j_{01}(j_{01}\\!\upharpoonright\\!(\mathscr{L}|\alpha))$,
we have

  1. 2.

$k:\mathscr{L}|\Theta\to\mathscr{L}|\Theta$ is elementary,

  2. 3.

$\mu_{1}$ is the measure derived from $k$ with seed
$k\\!\upharpoonright\\!V_{\lambda}$,

  3. 4.

$\mathrm{Ult}_{0}(\mathscr{L}|\Theta,\mu_{1})=\mathscr{L}|\Theta$ and $k$ is
the associated ultrapower map (so
$k\\!\upharpoonright\\!V_{\lambda}=i^{\mathscr{L}}_{\mu_{1}}\\!\upharpoonright\\!V_{\lambda}$),

  4. 5.

$\mathscr{L}|\Theta=j_{12}(\mathscr{L}|\Theta)$ and
$k=j_{12}\\!\upharpoonright\\!(\mathscr{L}|\Theta)$.

Let $\Gamma$, etc, be as above for $j=j_{01}$. Then:

  1. 6.

Los’ theorem holds for $\mathrm{Ult}_{0}(\mathscr{L},\mu_{1})$, and the
ultrapower is extensional and isomorphic to $\mathscr{L}$,

  2. 7.

for each $s\in\vec{\Gamma}$, we have
$j_{01}\\!\upharpoonright\\!H^{s}\in\mathscr{L}$ and

$j_{12}\\!\upharpoonright\\!H^{s}=j(j_{01}\\!\upharpoonright\\!H^{s}),$

so recalling
$\mathscr{L}=\mathrm{Hull}^{\mathscr{L}}(V_{\lambda+1}\cup\Gamma)$, we have
$j_{12}=\bigcup_{s\in\vec{\Gamma}}j_{01}(j_{01}\\!\upharpoonright\\!H^{s})$,

  3. 8.

$j_{12}\\!\upharpoonright\\!\Gamma=\mathrm{id}$.

###### Proof.

Part 1: Because $\alpha<\Theta$ there is a surjection
$\pi:V_{\lambda+1}\to\mathscr{L}|\alpha$ with $\pi\in\mathscr{L}$. But then
note that

$j_{01}\circ\pi=j_{01}(\pi)\circ j_{01},$

which suffices since $j_{01}(\pi)\in\mathscr{L}$ and
$j_{01}\\!\upharpoonright\\!V_{\lambda+1}\in\mathscr{L}$ (it is determined by
$j_{01}\\!\upharpoonright\\!V_{\lambda}$).

So let
$k=\bigcup_{\alpha<\Theta}j_{01}(j_{01}\\!\upharpoonright\\!(\mathscr{L}|\alpha))$.

Part 2: we get $\Sigma_{0}$-elementarity immediately, hence
$\Sigma_{1}$-elementarity by $\in$-cofinality. But then because
$L_{\Theta}(V_{\lambda+1})\models\mathsf{ZF}^{-}$, this implies full
elementarity.

Part 3: Let $\alpha<\Theta$. Then
$\bar{\mu}=\mu_{0}\cap\mathscr{L}|\alpha\in\mathscr{L}$ and
$\bar{j}=j_{01}\\!\upharpoonright\\!\mathscr{L}|\alpha$ and
$\bar{j}\\!\upharpoonright\\!V_{\lambda}=j_{01}\\!\upharpoonright\\!V_{\lambda}$.
Note $\mathscr{L}|\Theta\models$“$\bar{\mu}$ is the measure derived from
$\bar{j}$ with seed $\bar{j}\\!\upharpoonright\\!V_{\lambda}$”. So
$\mathscr{L}|\Theta\models$“$j_{01}(\bar{\mu})$ is the measure derived from
$j_{01}(\bar{j})$ with seed $j(\bar{j}\\!\upharpoonright\\!V_{\lambda})$”, but
$j_{01}(\bar{\mu})=\mu_{1}\cap j_{01}(\mathscr{L}|\alpha)$ and
$j_{01}(\bar{j})\subseteq k$ and
$j(\bar{j}\\!\upharpoonright\\!V_{\lambda})=k\\!\upharpoonright\\!V_{\lambda}$.
Since this holds for all $\alpha$, we are done.

Part 4: like the proper class case, but simpler.

Part 5: Let $f\in\mathscr{L}$ with $f:V_{\lambda+1}\to\mathscr{L}|\Theta$.
Then $\mathrm{rg}(f)\subseteq\mathscr{L}|\alpha$ for some $\alpha<\Theta$, so
easily $f\in\mathscr{L}|\Theta$, which by the previous part suffices.

Parts 6, 7: For $s\in[\Gamma]^{<\omega}\backslash\\{\emptyset\\}$, write
$\ell^{s}=(j_{01})^{s}\in\ell$. By elementarity of $j_{01}$ and since
$j_{01}(s)=s$,

$j_{01}(\ell^{s}):H^{s}\to H^{s}$

is the unique elementary map $\ell^{\prime}:H^{s}\to H^{s}$ such that
$\ell^{\prime}(s^{-})=s^{-}$ and
$\ell^{\prime}\\!\upharpoonright\\!V_{\lambda}=j_{01}(j_{01}\\!\upharpoonright\\!V_{\lambda})=k\\!\upharpoonright\\!V_{\lambda}$.
It follows that setting

$j^{\prime}=\bigcup_{s\in\vec{\Gamma}}j_{01}(\ell^{s}),$

we have $j^{\prime}:\mathscr{L}\to\mathscr{L}$ is cofinal
$\Sigma_{0}$-elementary, hence (by $\mathsf{ZF}$) fully elementary. Moreover,
$j^{\prime}\\!\upharpoonright\\!\mathscr{L}|\Theta=k$. But then the usual
calculations show that $\mathrm{Ult}(\mathscr{L},\mu_{1})$ satisfies Los’
theorem, is extensional, isomorphic to $\mathscr{L}$, and its ultrapower map
factors through $j^{\prime}$, and in fact $=j^{\prime}$, so we are done.

Part 8: This follows easily from the characterization of $j_{12}$ we just
gave.151515We could have alternatively just chosen $\Gamma$ to be fixed by the
relevant ultrapower maps, by standard considerations. ∎

######  Claim 2.

Let $j$ be a proper $I_{0}$-embedding. Then $j$ is
$(\omega+\omega+1)$-iterable.

###### Proof.

We have $j=j_{0}=i^{\mathscr{L}}_{\mu_{0}}:\mathscr{L}\to\mathscr{L}$ and and
$j_{1}=i^{\mathscr{L}}_{\mu_{1}}:\mathscr{L}\to\mathscr{L}$ (and the
ultrapower satisfies Los’ theorem, is extensional and isomorphic to
$\mathscr{L}$) by Lemma 1. Fix $\Gamma$, etc, as above. So
$j_{0}\\!\upharpoonright\\!\Gamma=\mathrm{id}$, $j^{s}:H^{s}\to H^{s}$ for
$s\in\vec{\Gamma}$,

$j_{0}=\bigcup_{s\in\vec{\Gamma}}(j_{0})^{s}\text{ and
}j_{1}=\bigcup_{s\in\vec{\Gamma}}j_{0}((j_{0})^{s}),$

and $j_{1}\\!\upharpoonright\\!\Gamma=\mathrm{id}$. But then we have the same
circumstances with $(\mathscr{L},j_{1},\mu_{1},\Gamma)$ as with
$(\mathscr{L},j_{0},\mu_{0},\Gamma)$, so we can iterate the process through
all $n<\omega$. So $(\mathscr{L},\mu_{0})$ is $\omega$-iterable, and the
ultrapower map by $\mu_{n}$ is the resulting function $j_{n}$ given by
iterating the process above.

Write $\left<\mathscr{L}_{m}\right>_{m\leq\omega}$ for the first $(\omega+1)$
iterates (so $\mathscr{L}_{m}=\mathscr{L}$ for $m<\omega$), and
$j_{mn}:\mathscr{L}_{m}\to\mathscr{L}_{n}$, for $0\leq m\leq n\leq\omega$, the
iteration maps. We next show that $\mathscr{L}_{\omega}$ is
wellfounded.161616At this point, Woodin’s argument in [21] seems to use some
$\mathsf{DC}$. We avoid this by arguing more like in the standard proof of
linear iterability, adapted to the “covering system” setup.

For $\ell<\omega$ and $\alpha\in\mathrm{OR}$, say $\alpha$ is _$(j_{0},\ell)$
-stable_ iff $j_{\ell n}(\alpha)=\alpha$ for all $n\in[\ell,\omega)$. Likewise
for $s\in[\mathrm{OR}]^{<\omega}$ (where we require $j_{\ell n}(s)=s$).

Let
$\vec{\mathrm{OR}^{\prime}}=[\mathrm{OR}\backslash(\lambda+1)]^{<\omega}\backslash\\{\emptyset\\}$.
Given an elementary $k:V_{\lambda}\to V_{\lambda}$, define the finite
_iterates_ of $k$, as far as possible, as follows: Start with $k_{0}=k$. Given
$k_{n}$, if $(k_{n})^{+}$ (the canonical extension) is elementary
$V_{\lambda+1}\to V_{\lambda+1}$ then let $k_{n+1}=(k_{n})^{+}(k_{n})$;
otherwise $k_{n+1}$ is not defined. By the preceding observations, $j_{n}$
exists for each $n<\omega$. Now given $s\in\vec{\mathrm{OR}^{\prime}}$, write
$\pi^{k,s}_{m,m+1}$ for the unique elementary map $\pi:H^{s}\to H^{s}$ such
that $\pi\\!\upharpoonright\\!V_{\lambda}=k_{m}$ (the $m$th iterate of $k$)
and $\pi(s^{-})=s^{-}$, if such exists; otherwise $\pi^{k,s}_{m,m+1}$ is not
defined.

######  Sublaim.

For each $\alpha\in\mathrm{OR}$ there is $\ell<\omega$ such that $\alpha$ is
$(j_{0},\ell)$-stable.

###### Proof.

Suppose otherwise and let $\alpha$ be least such. Let $s\in\vec{\Gamma}$ with
$\alpha\in H^{s}$. Note then that $\mathscr{L}$ satisfies the statement, in
parameters $\alpha$, $s$, $j_{01}\\!\upharpoonright\\!V_{\lambda}$, “$\alpha$
is the least $\beta\in\mathrm{OR}\cap H^{s}$ such that

$\pi^{(j_{01}\\!\upharpoonright\\!V_{\lambda}),s}_{m,m+1}(\beta)>\beta$

for cofinally many $m<\omega$”. But then applying $j_{0n}$ to this statement
with some $n$ such that $\alpha^{\prime}=j_{0n}(\alpha)>\alpha$, we get
$\mathscr{L}_{n}=\mathscr{L}$ satisfies the statement, in parameters
$\alpha^{\prime}$, $s$, $j_{n,n+1}\\!\upharpoonright\\!V_{\lambda}$,
“$\alpha^{\prime}$ is the least $\beta\in\mathrm{OR}\cap H^{s}$ such that

$\pi^{j_{n,n+1}\\!\upharpoonright\\!V_{\lambda},s}_{m,m+1}(\beta)>\beta$

for cofinally many $m<\omega$”, but then clearly $\alpha^{\prime}=\alpha$, a
contradiction.∎

Using the hulls and maps defined above, $\mathscr{L}$ can form a covering
system for the direct limit, just like the standard covering systems
considered in inner model theory and/or in [21], with some direct limit
$\widetilde{\mathscr{L}_{\omega}}$, which we will eventually show
$=\mathscr{L}_{\omega}$. This proceeds as follows. For $k:V_{\lambda}\to
V_{\lambda}$ elementary and $s\in\vec{\mathrm{OR}^{\prime}}$, say that $s$ is
_$k$ -potentially-stable_ iff for all $m<\omega$, the map $\pi^{k,s}_{m,m+1}$
exists (hence is elementary $H^{s}\to H^{s}$ etc). Similarly, for
$\ell<\omega$, we say that $s$ is _$(k,\ell)$ -potentially-stable_ iff this
holds for all $m\geq\ell$. If $s$ is $(k,\ell)$-potentially-stable and
$\ell\leq m\leq n$ let $\pi^{k,s}_{mn}:H^{s}\to H^{s}$ be defined naturally by
composition. That is, $\pi^{k,s}_{mm}=\mathrm{id}$, $\pi^{k,s}_{m,m+1}$ is
already defined, and $\pi^{k,s}_{m,n+1}=\pi^{k,s}_{n,n+1}\circ\pi^{k,s}_{mn}$.

Note that if $\alpha\in\mathrm{OR}$ is $(j_{0},\ell)$-stable then $\alpha$ is
$(j_{0}\\!\upharpoonright\\!V_{\lambda},\ell)$-potentially-stable, and hence
for every $s\in[\mathrm{OR}]^{<\omega}$ there is $\ell<\omega$ such that $s$
is $(j_{0}\\!\upharpoonright\\!V_{\lambda},\ell)$-potentially-stable.

For $k:V_{\lambda}\to V_{\lambda}$, let $\mathscr{P}^{k}$ be the class of
pairs $(s,\ell)$ such that $s\in\vec{\mathrm{OR}^{\prime}}$ and $s$ is
$(k,\ell)$-potentially-stable. For $(s,\ell),(t,m)\in\mathscr{P}_{k}$ let
$(s,\ell)\leq(t,m)$ iff $s\subseteq t$ and $\ell\leq m$, and in this case,
define

$\pi^{k,s,t}_{mn}:H^{s}\to H^{t}$

to have the same graph as has $\pi^{k,s}_{mn}$; so $\pi^{k,s,t}_{mn}$ is then
$\Sigma_{0}$-elementary.

Say that $k$ is _valid_ if for every $s\in[\mathrm{OR}]^{<\omega}$ there is
$n<\omega$ such that $(s,k)\in\mathscr{P}^{k}$. So
$j_{0}\\!\upharpoonright\\!V_{\lambda}$ is valid. Assume now that $k$ is
valid. Note then that $\mathscr{P}^{k}$ is directed and the embeddings
$\pi^{k,s,t}_{mn}$ commute; that is, if $(s,\ell)\leq(t,m)\leq(u,n)$ then

$\pi^{k,s,u}_{\ell n}=\pi^{k,t,u}_{mn}\circ\pi^{k,s,t}_{\ell m}.$

So we define the directed system

$\mathscr{D}^{k}=\left<H^{s},H^{t};\pi^{k,s,t}_{mn}\bigm{|}(s,m)\leq(t,n)\in\mathscr{P}^{k}\right>.$

Let $\widetilde{\mathscr{L}}^{k}_{\omega}$ be its direct limit, and
$\pi^{k,s}_{m\omega}:H^{s}\to\widetilde{\mathscr{L}}^{k}_{\omega}$ the direct
limit map. Note that $\mathscr{P}^{k}$, validity, $\mathscr{D}^{k}$,
$\widetilde{\mathscr{L}}^{k}_{\omega}$ and $\pi^{k,s}_{m\omega}$ are all
definable over $\mathscr{L}$, and uniformly so in $k$ etc.

Now if $(s,\ell)\in\mathscr{P}^{j_{n}\\!\upharpoonright\\!V_{\lambda}}$ and
$s$ is $(j_{n}\\!\upharpoonright\\!V_{\lambda},\ell)$-truly-stable and
$\ell\leq m<\omega$ then

$j_{n+\ell,n+m}\\!\upharpoonright\\!H^{s}=\pi^{j_{n}\\!\upharpoonright\\!V_{\lambda},s}_{\ell,m}.$

So working in $V$, we can define

$\sigma_{n}:\widetilde{\mathscr{L}}^{j_{n}\\!\upharpoonright\\!V_{\lambda}}_{\omega}\to\mathscr{L}_{\omega}$

by setting

$\sigma_{n}(\pi^{j_{n}\\!\upharpoonright\\!V_{\lambda},s}_{\ell\omega}(x))=j_{n+\ell,\omega}(x)$

whenever $s$ is $(j_{n}\\!\upharpoonright\\!V_{\lambda},\ell)$-stable and
$x\in H^{s}$. Clearly
$\widetilde{\mathscr{L}}^{j_{n}\\!\upharpoonright\\!V_{\lambda}}_{\omega}$ and
$\sigma_{n}$ are independent of $n$, so just write
$\widetilde{\mathscr{L}}_{\omega},\sigma$.

Now $\widetilde{\mathscr{L}}_{\omega}=\mathscr{L}_{\omega}$ and
$\sigma=\mathrm{id}$, because for each $x\in\mathscr{L}$ there is
$s\in\vec{\Gamma}$ such that $x\in H^{s}$, so for any $n<\omega$, noting that
$s$ is $(j_{0}\\!\upharpoonright\\!V_{\lambda},n)$-stable, we then get
$j_{n\omega}(x)=\sigma(\pi^{j_{0}\\!\upharpoonright\\!V_{\lambda},s}_{n\omega}(x))$,
so $j_{n\omega}(x)\in\mathrm{rg}(\sigma)$, as desired.

######  Sublaim 1.

$\mathscr{L}_{\omega}$ is wellfounded.

###### Proof.

Suppose not. Then there is a least $\alpha\in\mathrm{OR}$ such that
$j_{0\omega}(\alpha)$ is in the illfounded part of $\mathscr{L}_{\omega}$. Let
$s\in\vec{\Gamma}$ with $\alpha\in H^{s}$. Using the covering system above, we
have a definition of $\mathscr{L}_{\omega}$ over $\mathscr{L}$ from the
parameter $j_{0}\\!\upharpoonright\\!V_{\lambda}$, and the illfounded part can
be computed by $\mathscr{L}$. Note then that $\mathscr{L}$ satisfies the
statement (in parameters $\alpha$, $s$,
$j_{0}\\!\upharpoonright\\!V_{\lambda}$)
“$(s,0)\in\mathscr{P}^{j_{0}\\!\upharpoonright\\!V_{\lambda}}$ and $\alpha$ is
the least $\beta\in\mathrm{OR}\cap H^{s}$ such that
$\pi^{j_{0}\\!\upharpoonright\\!V_{\lambda},s}_{0\omega}(\beta)$ is in the
illfounded part of $\mathscr{L}_{\omega}$”. Now let $m<\omega$ be such that
there is $\alpha_{1}<j_{0m}(\alpha)$ and $j_{m\omega}(\alpha_{1})$ is in the
illfounded part. Let $t\in\vec{\Gamma}$ with $s\subseteq t$ and $\alpha_{1}\in
H^{t}$. Note that we may in fact assume that $s=t$, by enlarging $s$ in the
first place, because this does not affect the minimality of $\alpha$ there.
Therefore applying $j_{0m}$ to the first statement and letting
$\alpha^{\prime}=j_{0m}(\alpha)$, we have
$\mathscr{L}\models$“$\alpha^{\prime}$ is the least $\beta\in\mathrm{OR}\cap
H^{s}$ such that
$\pi^{j_{m}\\!\upharpoonright\\!V_{\lambda},s}_{0\omega}(\beta)$ is in the
illfounded part of $\mathscr{L}_{\omega}$” (noting here that
$\mathscr{L}_{\omega}$ is defined in the same manner from
$j_{0}\\!\upharpoonright\\!V_{\lambda}$ or
$j_{m}\\!\upharpoonright\\!V_{\lambda}$). But this contradicts the choice of
$\alpha_{1}<\alpha^{\prime}$ and $m$ and $t=s$. ∎

We now define the usual $*$-map: For $\alpha\in\mathrm{OR}$ let

$\alpha^{*}=\pi^{j_{0}\\!\upharpoonright\\!V_{\lambda},s}_{n\omega}(\alpha)$

whenever $\alpha\in s^{-}$ and $n$ is large enough. Then it is easy to see
that $\alpha^{*}=\lim_{n<\omega}j_{n\omega}(\alpha)$, but considering the
first definition given above, we have:

######  Claim 3.

The map $\mathrm{OR}\to\mathrm{OR}$ given by $\alpha\mapsto\alpha^{*}$, is
definable over $\mathscr{L}$ from the parameter
$j_{n}\\!\upharpoonright\\!V_{\lambda}$, uniformly in $n<\omega$.

Now let
$\Gamma^{*}=j_{0\omega}``\Gamma=\\{\alpha^{*}\bigm{|}\alpha\in\Gamma\\}$. Then
clearly
$\mathscr{L}_{\omega}=\mathrm{Hull}^{\mathscr{L}_{\omega}}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}\cup\Gamma^{*})$.
Define $\widetilde{j}_{\omega,\omega+1}$ by pushing $j_{01}$ through as
before; that is, for each $s\in\vec{\Gamma}$,

$\widetilde{j}_{\omega,\omega+1}\\!\upharpoonright\\!(H^{s^{*}})^{\mathscr{L}_{\omega}}=j_{0\omega}((j_{0})^{s}).$

Much as before, in fact $\widetilde{j}_{\omega,\omega+1}=j_{\omega,\omega+1}$
(the ultrapower map given by $\mu_{\omega}$), and
$\mathrm{Ult}(\mathscr{L}_{\omega},\mu_{\omega})=\mathscr{L}_{\omega}$ etc.
Moreover,
$\widetilde{j}_{\omega,\omega+1}\\!\upharpoonright\\!\Gamma^{*}=\mathrm{id}$.
So we have the same circumstances at stage $\omega$ that we had at stage $0$
(without the true $V_{\lambda_{\omega}+1}$, but that isn’t relevant).
Therefore by the same proof, we reach $(\omega+\omega+1)$-iterability (in fact
$\omega^{2}$-iterability). ∎

So we have the iterates
$(\mathscr{L}_{\alpha},\lambda_{\alpha},\mu_{\alpha},j_{\alpha})$ for
$\alpha\leq 2\cdot\omega$, and the models $\mathcal{L}_{\alpha}$ are definable
in $\mathscr{L}$ from the parameter $j_{0}\\!\upharpoonright\\!V_{\lambda}$.
(Note $V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}$ is just the direct limit
of $V_{\lambda+1}$ under the maps $j_{n}\\!\upharpoonright\\!V_{\lambda+1}$,
etc. So we don’t even need the covering system mentioned above for this.)

Note $\lambda_{\omega}=j_{0\omega}(\lambda)<\Theta$ and in fact $\mathscr{L}$
has a surjection $\pi:V_{\lambda+1}\to
V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}$. Since
$\mathscr{L}_{\omega}\subseteq\mathscr{L}$, it follows that
$j_{0\omega}(\Theta)=\Theta$. Note $j_{0\omega}$ is continuous at $\Theta$.

Now $\mathscr{L}_{\omega}$ has the sequence
$\left<j_{\omega+n}\\!\upharpoonright\\!V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}\right>$,
and defines $\mathscr{L}_{\omega+\omega}=j_{0\omega}(\mathscr{L}_{\omega})$.
In $V$ we have the iteration map
$j_{\omega,\omega+\omega}:\mathscr{L}_{\omega}\to\mathscr{L}_{\omega+\omega}$.
We can now prove, with basically the usual argument:

######  Claim 4.

$\alpha^{*}=j_{\omega,\omega+\omega}(\alpha)$ for all $\alpha\in\mathrm{OR}$.

###### Proof.

Fix $\alpha$. Let $n<\omega$ and $\bar{\alpha}$ be such that
$j_{n\omega}(\bar{\alpha})=\alpha$ and $\alpha$ is $(j_{0},n)$-stable. Let
$s\in\vec{\Gamma}$ with $\bar{\alpha}\in H^{s}$ and let
$k=j_{n}\\!\upharpoonright\\!V_{\lambda}$. Then

$\mathscr{L}=\mathscr{L}_{n}\models\pi^{k,s}_{0\omega}(\bar{\alpha})=\alpha.$

We have $s^{*}=j_{n\omega}(s)\in\vec{\Gamma^{*}}$ and
$\alpha^{*}=j_{n\omega}(\alpha)$, so letting
$k^{\prime}=j_{\omega}\\!\upharpoonright\\!V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}=j_{n\omega}(k)$,

$\mathscr{L}_{\omega}\models\pi^{k^{\prime},s^{*}}_{0\omega}(\alpha)=\alpha^{*}$

(the two superscript-$*$s are as computed in $\mathscr{L}$, not
$\mathscr{L}_{\omega}$). But

$(\pi^{k^{\prime},s^{*}}_{0\omega}(\alpha))^{\mathscr{L}_{\omega}}=j_{\omega,\omega+\omega}(\alpha),$

since $j_{\omega}(s^{*})=s^{*}$ (and by basically the same calculations as
earlier with $\mathscr{L}_{\omega}$ replacing $\mathscr{L}$). ∎

Given $C\subseteq\mathscr{L}_{\omega}$, write
$\mathscr{L}_{\omega}[C]=L(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}},C)$.
We are interested in $\mathscr{L}_{\omega}[*]$,
$\mathcal{L}_{\omega}[j_{\omega}]$ and
$\mathscr{L}_{\omega}[j_{\omega,\omega+\omega}]$. Given a transitive proper
class $N\models\mathsf{ZF}$, we say that a class $C\subseteq N$ is _amenable_
to $N$ iff $C\cap V_{\alpha}\in N$ for each $\alpha\in\mathrm{OR}$.

So $j_{\omega,\omega+\omega}\\!\upharpoonright\\!\mathrm{OR}$ is amenable to
$\mathcal{L}_{\omega}[*]$. Since already
$j_{\omega,\omega+\omega}\\!\upharpoonright\\!V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}\in\mathscr{L}_{\omega}$,
it follows that the full embedding $j_{\omega,\omega+\omega}$ is amenable to
$\mathscr{L}_{\omega}[*]$, and in fact,
$\mathscr{L}_{\omega}[*]=\mathscr{L}_{\omega}[j_{\omega,\omega+\omega}]$ and
$j_{\omega,\omega+\omega}$ is definable over $\mathscr{L}_{\omega}[*]$ from
the predicate $*$ and parameter
$j_{\omega,\omega+\omega}\\!\upharpoonright\\!V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}$.
We will refine this somewhat in Claim 6 below. But first we prove the key
fact:

######  Claim 5.

$V_{\lambda_{\omega}+2}^{\mathscr{L}_{\omega}}=V_{\lambda_{\omega}+2}^{\mathscr{L}_{\omega}[*]}$.

###### Proof.

Note that for $m\leq n<\omega$ we have
$j_{mn}(\mathscr{L}_{\omega})=\mathscr{L}_{\omega}$ and $j_{mn}(*)=*$. So
$j_{mn}(\mathscr{L}_{\omega}[*])=\mathscr{L}_{\omega}[*]$. Let $X\subseteq
V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}[*]}$ with
$X\in\mathscr{L}_{\omega}[*]$. Now
$\mathscr{L}_{\omega}[*]=L(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}},*)$,
and $*\subseteq\mathrm{OR}$. So there are $\eta\in\mathrm{OR}$ and $y\in
V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}$ such that for all $x\in
V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}$, we have

$x\in X\iff\mathscr{L}_{\omega}[*]\models\varphi(x,y,\eta,*)$

(where the reference to $*$ in $\varphi$ is literally via a predicate). Let
$n<\omega$ such that $\eta$ is
$(j_{0}\\!\upharpoonright\\!V_{\lambda},n)$-stable and
$y\in\mathrm{rg}(j_{n\omega})$ and let $j_{n\omega}(\bar{y})=y$. Let
$k_{n\omega}=j_{n\omega}\\!\upharpoonright\\!V_{\lambda+1}$. Working in
$\mathscr{L}=\mathscr{L}_{n}$, define $\bar{X}$ by setting

$\bar{x}\in\bar{X}\iff\bar{x}\in V_{\lambda+1}\text{ and
}\mathscr{L}_{\omega}[*]\models\varphi(k_{n\omega}(\bar{x}),k_{n\omega}(\bar{y}),\eta,*).$

Let $X^{\prime}=j_{n\omega}(\bar{X})$. Then note that $X^{\prime}=X$, so
$X\in\mathscr{L}_{\omega}$, as desired. ∎

######  Claim 6.

We have:

  1. 1.

$\mathscr{L}_{\omega}[j_{\omega}]=\mathscr{L}_{\omega}[j_{\omega,\omega+\omega}]=\mathscr{L}_{\omega}[*]=\mathscr{L}_{\omega}[j_{\omega}\\!\upharpoonright\\!\Theta]$.

  2. 2.

$j_{\omega}$, $j_{\omega,\omega+\omega}$, and $*$ are definable over
$\mathscr{L}_{\omega}[j_{\omega}]$ from the parameters
$j_{\omega}\\!\upharpoonright\\!\Theta$ and
$j_{\omega}\\!\upharpoonright\\!V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}$.

###### Proof.

We already know that
$\mathscr{L}_{\omega}[j_{\omega,\omega+\omega}]=\mathscr{L}_{\omega}[*]$. And
clearly $j_{\omega,\omega+\omega}$ is computable from
$j_{\omega,\omega+1}=j_{\omega}$.

Now to compute $j_{\omega}=j_{\omega,\omega+1}$ in
$\mathscr{L}_{\omega}[j_{\omega,\omega+\omega}]$, it suffices to compute
$j_{\omega,\omega+1}\\!\upharpoonright\\!V_{\lambda_{\omega}+2}^{\mathscr{L}_{\omega}}$,
since this gives $\mu_{\omega}$. But given $X\in
V_{\lambda_{\omega}+2}^{\mathscr{L}_{\omega}}$, we have
$X^{\prime}=j_{\omega,\omega+1}(X)\subseteq
V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}$, and

$x\in X^{\prime}\iff j_{\omega+1,\omega+\omega}(x)\in
j_{\omega+1,\omega+\omega}(X^{\prime})=j_{\omega,\omega+\omega}(X),$

and
$j_{\omega+1,\omega+\omega}\\!\upharpoonright\\!V_{\lambda_{\omega}^{\mathscr{L}_{\omega}}+1}\in\mathscr{L}_{\omega}$,
so using $j_{\omega,\omega+\omega}$, this computes $X^{\prime}$, uniformly in
$X$.

Also, working in
$\mathscr{L}_{\omega}[j_{\omega}\\!\upharpoonright\\!\Theta]$, we can compute
$j_{\omega}\\!\upharpoonright\\!L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})$
from the parameters $j_{\omega}\\!\upharpoonright\\!\Theta$ and
$j_{\omega}\\!\upharpoonright\\!V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}$
(using the canonical extension to compute
$j_{\omega}\\!\upharpoonright\\!V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}$),
and since $V_{\lambda_{\omega}+2}^{\mathscr{L}}\subseteq
L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})$, this computes
$\mu_{\omega}$ and hence the full class embeddings. ∎

By the claims, we have
$\mathscr{L}_{\omega}[j_{\omega}]\models$“$V_{\lambda_{\omega}+2}\subseteq
L(V_{\lambda_{\omega}+1})$”. So we have the version of part 1 of the theorem
given by replacing $\mathscr{L}[j]$ with $\mathscr{L}_{\omega}[j_{\omega}]$.

Finally we let

$H=\mathrm{Hull}^{\mathscr{L}_{\omega}[j_{\omega}]}(\mathrm{rg}(j_{0\omega})\cup\\{j_{\omega}\\!\upharpoonright\\!\Theta\\})=\mathrm{Hull}^{\mathscr{L}_{\omega}[j_{\omega}]}(\mathrm{rg}(j_{0\omega})\cup\\{*\\})$

(the notation for the hull on the right is supposed to mean that the class $*$
is available as a predicate; the two hulls are of course identical by the
previous claims). We use a variant of the argument from [18] to prove Claim 8
below (we need a little extra argument which does not show up in the mouse
case), which relies on the easily verified Claim 7:

######  Claim 7.

Given $x\in\mathscr{L}_{\omega}$, if $x\in\mathrm{rg}(j_{n\omega})$ then
$j_{nm}(x)=x$ for all $m\in[n,\omega)$.

###### Proof.

Let $\bar{x}$ with $j_{n\omega}(\bar{x})=x$ and let $s\in\vec{\Gamma}$ be such
that $\bar{x}\in H^{s}$. Then
$\mathscr{L}=\mathscr{L}_{n}\models$“$x=\pi^{j_{n}\\!\upharpoonright\\!V_{\lambda},s}_{0\omega}(\bar{x})$”,
so letting $x^{\prime}=j_{nm}(x)$ and $\bar{x}^{\prime}=j_{nm}(\bar{x})$, we
have
$\mathscr{L}\models$“$x^{\prime}=\pi^{j_{m}\\!\upharpoonright\\!V_{\lambda},s}_{0\omega}(\bar{x}^{\prime})$”,
but
$\pi^{j_{m}\\!\upharpoonright\\!V_{\lambda},s}_{0\omega}(\bar{x}^{\prime})=j_{m\omega}(\bar{x}^{\prime})=x$.
∎

We have already defined $\alpha^{*}$ for $\alpha\in\mathrm{OR}$; using the
preceding claim, we now extend this function to $\mathscr{L}_{\omega}$. For
$(s,n)\in\mathscr{P}^{j_{0}\\!\upharpoonright\\!V_{\lambda}}$ and $x\in
H^{s}\cap\mathscr{L}_{\omega}$, let

$x^{*}=\pi_{n\omega}^{j_{0}\\!\upharpoonright\\!V_{\lambda},s}(x),$

or equivalently, $x^{*}=\lim_{n\to\omega}j_{n\omega}(x)$. Just as in the proof
of Claim 4, we have $x^{*}=j_{\omega,\omega+\omega}(x)$ for all
$x\in\mathscr{L}_{\omega}$. So $x\mapsto x^{*}$, with domain
$\mathscr{L}_{\omega}$, is definable over
$\mathscr{L}_{\omega}[j_{\omega}\\!\upharpoonright\\!\Theta]$ just like
$*\\!\upharpoonright\\!\mathrm{OR}$ is.

######  Claim 8.

(i) $H\cap\mathscr{L}_{\omega}=\mathrm{rg}(j_{0\omega})$ and (ii)
$H\preccurlyeq\mathscr{L}_{\omega}[j_{\omega}]$.

###### Proof.

Part (i): Let $z\in H\cap\mathscr{L}_{\omega}$. We first observe that
$j_{0n}(z)=z$ for all $n<\omega$, and so
$z^{*}=j_{0\omega}(z)\in\mathrm{rg}(j_{0\omega})$. To see this, fix
$x\in\mathrm{rg}(j_{0\omega})$ and a formula $\varphi$ such that

$\mathscr{L}_{\omega}[*]\models z\text{ is the unique }z^{\prime}\text{ such
that }\varphi(z^{\prime},x,*).$

(note this statement is in “parameters” $z$, $x$ and $*$). Applying $j_{0n}$
gives the following, in “parameters” $j_{0n}(z)$ and $x=j_{0n}(x)$ and $*$:

$\mathscr{L}_{\omega}[*]\models j_{0n}(z)\text{ is the unique
}z^{\prime}\text{ such that }\varphi(z^{\prime},x,*);$

we use here that $j_{0n}$ fixes $\mathscr{L}_{\omega}$, $*$ and $x$, by Claim
7. So $j_{0n}(z)=z$.

But for (i) we need $z\in\mathrm{rg}(j_{0\omega})$, not $z^{*}$. For this, let
$s\in\vec{\Gamma}$ (so $s^{*}\in\vec{\Gamma^{*}}$) be such that
$z\in(H^{s^{*}})^{\mathscr{L}_{\omega}}$. Now
$j_{0\omega}\\!\upharpoonright\\!H^{s}:H^{s}\to(H^{s^{*}})^{\mathscr{L}_{\omega}}$
is the unique elementary map $\pi$ such that
$j_{0\omega}\\!\upharpoonright\\!V_{\lambda}\subseteq\pi$ and
$\pi(s^{-})=(s^{*})^{-}$, and easily then
$j_{0\omega}\\!\upharpoonright\\!H^{s}\in\mathscr{L}$, and since also
$s^{*}\in\vec{\Gamma^{*}}$, it easily follows that

$j_{\omega,\omega+\omega}\\!\upharpoonright\\!(H^{s^{*}})^{\mathscr{L}_{\omega}}=j_{0\omega}(j_{0\omega}\\!\upharpoonright\\!H^{s})\in\mathrm{rg}(j_{0\omega}).$

But $z\in(H^{s^{*}})^{\mathscr{L}_{\omega}}$, and we have seen that
$z^{*}=j_{\omega,\omega+\omega}(z)$ and both $z^{*}$ and
$\bar{j}=j_{\omega,\omega+\omega}\\!\upharpoonright\\!(H^{s^{*}})^{\mathscr{L}_{\omega}}$
are in $\mathrm{rg}(j_{0\omega})$. But then
$z=\bar{j}^{-1}(z^{*})\in\mathrm{rg}(j_{0\omega})$, as desired.

Now consider (ii). We have $\mathscr{L}_{\omega}[*]=\mathscr{L}_{\omega}[k]$
where $k=j_{\omega}\\!\upharpoonright\\!\Theta$, and for convenience we deal
with the latter form. Let $x\in\mathrm{rg}(j_{0\omega})$ and suppose that

$\mathscr{L}_{\omega}[k]\models\exists z\ \varphi(z,x,k),$

and $m<\omega$ where $\varphi$ is $\Sigma_{m}$. We want some $z\in H$ such
that $\mathscr{L}_{\omega}[k]\models\varphi(z,x,k)$. Let $\eta\in\mathrm{OR}$
with $\Theta<\eta$ and $x\in
L_{\eta}(V_{\lambda+1})\preccurlyeq_{m+10}\mathscr{L}$ and
$j_{0\omega}(\eta)=\eta$ (we can find such $\eta$ because $j_{0\omega}$ arises
from a sequence of ultrapowers). Then because of how $\mathscr{L}_{\omega}[k]$
is defined in $\mathscr{L}$, we have

$(\mathscr{L}_{\omega}[k])|\eta\preccurlyeq_{m+1}\mathscr{L}_{\omega}[k].$

Let

$J=\mathrm{Hull}^{(\mathscr{L}_{\omega}[k])|\eta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}\cup\\{x,k\\});$

then $J\preccurlyeq(\mathscr{L}_{\omega}[k])|\eta$ since
$V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}\cup\\{k\\}\subseteq J$. Let $C$
be the transitive collapse of $J$ and $\pi:C\to J$ the uncollapse map. Let
$\pi(x^{C})=x$.

Now we claim that $C,x^{C}\in\mathrm{rg}(j_{0\omega})$ and $\pi\in H$. For we
defined $C,x^{C},\pi$ in $\mathscr{L}_{\omega}[k]$ from the parameters
$\eta=j_{0\omega}(\eta)$, $x$ and $k$, so they are in $H$. But $C,x^{C}$ are
also coded by elements of
$V_{\lambda_{\omega}+2}^{\mathscr{L}_{\omega}[k]}=V_{\lambda_{\omega}+2}^{\mathscr{L}_{\omega}}$
(the equality by Claim 5), so $C,x^{C}\in\mathscr{L}_{\omega}\cap H$, so
$C,x^{C}\in\mathrm{rg}(j_{0\omega})$ by part (i).

So write $j_{0\omega}(C_{0},x^{C_{0}})=(C,x^{C})$. Since $\pi\in H$, we have
$\pi``(j_{0\omega}``C_{0})\subseteq H$. But $\pi$ is elementary, so
$C\models\exists z\varphi(z,x^{C})$, so $C_{0}\models\exists
z\varphi(z,x^{C_{0}})$. So fixing a $z_{0}\in C_{0}$ witnessing this, then
$z=\pi(j_{0\omega}(z_{0}))$ is as desired. ∎

Since $H\preccurlyeq\mathscr{L}_{\omega}[j_{\omega}]$, $H$ is extensional, so
we can let $N$ be its transitive collapse and
$\widehat{j}_{0\omega}:N\to\mathscr{L}_{\omega}[j_{\omega}]$ the uncollapse
map.

######  Claim 9.

We have:

  1. –

$N=\mathscr{L}[j]=\mathscr{L}[j\\!\upharpoonright\\!\Theta]$ and $j$ is
definable over $\mathscr{L}[j]$ from the parameter
$j\\!\upharpoonright\\!(V_{\lambda}\cup\Theta)$.

  2. –

$j_{0\omega}\subseteq\widehat{j}_{0\omega}:\mathscr{L}[j]\to\mathscr{L}_{\omega}[j_{\omega}]$
is elementary.

###### Proof.

By the previous claim, $\mathscr{L}\subseteq N=L(V_{\lambda+1})^{N}$ and
$\widehat{j}_{0\omega}\\!\upharpoonright\\!\mathscr{L}=j_{0\omega}$. But
$j\\!\upharpoonright\\!\alpha\in\mathscr{L}$ for all $\alpha<\Theta$ and
$j_{0\omega}(j\\!\upharpoonright\\!\alpha)=j_{\omega}\\!\upharpoonright\\!j_{0\omega}(\alpha)$,
so
$\widehat{j}_{0\omega}(j\\!\upharpoonright\\!\Theta)=j_{\omega}\\!\upharpoonright\\!\Theta$,
so $N=\mathscr{L}[j]=\mathscr{L}[j\\!\upharpoonright\\!\Theta]$. ∎

So the first order theory of $(\mathscr{L}[j],\mathscr{L})$ is exactly that of
$(\mathscr{L}_{\omega}[j_{\omega}],\mathscr{L}_{\omega})$, and part 1 (for
$\mathscr{L}[j]$) follows immediately from what we know about
$\mathscr{L}_{\omega}[j_{\omega}]$.

Part 2: These statements are mostly direct consequences of the definitions and
part 1. For part 2(d), i.e. that $\Theta$ is still regular in
$\mathscr{L}[j_{0}]$: We have
$\Theta=\Theta_{\lambda+1}^{\mathscr{L}[j]}=\Theta_{\lambda+1}^{\mathscr{L}}=\Theta_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}$
and $\mathscr{L}_{\omega}[j_{\omega}]\subseteq\mathscr{L}$, so $\Theta$ is
regular in $\mathscr{L}_{\omega}[j_{\omega}]$, so by elementarity, $\Theta$ is
regular in $\mathscr{L}[j]$. Alternatively, notice that if $f:\alpha\to\Theta$
is cofinal where $\alpha<\Theta$, then for each $\beta<\alpha$ we can select
the least $\gamma<\Theta$ such that $f(\beta)<\gamma$ and
$\mathscr{L}|\gamma=\mathrm{Hull}^{\mathscr{L}|\gamma}(V_{\lambda+1})$, (since
this happens cofinally often below $\Theta$), and put the resulting sequence
of theories $\operatorname{Th}^{\mathcal{L}|\gamma}(V_{\lambda+1})$ together,
and form a new subset of $V_{\lambda+1}$, a contradiction.

Part 3 ($\mu_{j}$ is fully iterable, for $\mathscr{L}$ and $\mathscr{L}[j]$,
and $j_{\alpha\beta}\subseteq j^{+}_{\alpha\beta}$): The fact that the
ultrapower $\mathrm{Ult}_{0}(\mathscr{L}[j],\mu_{j})$ satisfies Los’ theorem
is similar to the proof of wellfoundedness, so we just discuss the latter
explicitly. Suppose the ultrapower is illfounded. Let $\eta\in\mathrm{OR}$ be
large and form

$\mathrm{Hull}^{(\mathscr{L}[j]|\eta,j\\!\upharpoonright\\!\eta)}(V_{\lambda+1}).$

This hull is fully elementary, and (by choice of $\eta$)
$j\\!\upharpoonright\\!\eta$ determines
$j\\!\upharpoonright\\!L_{\eta}(V_{\lambda+1})$ and hence $\mu_{j}$. Let $C$
be the transitive collapse of the hull. Then the illfoundedness reflects into
$\mathrm{Ult}_{0}(C,\mu_{j}\cap C)$. (Here we don’t need to construct a
specific $\in$-descending sequence; the illfounded part of the ultrapower is
computed in a first order fashion, so by elementarity, functions representing
objects in the illfounded part of
$\mathrm{Ult}_{0}(\mathscr{L}[j]|\eta,\mu_{j})$ also represent objects in the
illfounded part of $\mathrm{Ult}_{0}(C,\mu_{j}\cap C)$). As $C$ is the
surjective image of $V_{\lambda+1}$, we get $C\in\mathscr{L}|\Theta$. But then
$\mathrm{Ult}_{0}(C,\mu_{j})$ gets absorbed into $j(C)$, which is transitive,
a contradiction.

So $\mathrm{Ult}_{0}(\mathscr{L}[j],\mu_{j})$ is wellfounded and satisfies
Los’ theorem. But then since $\mu_{j}\in\mathscr{L}[j]$, the usual argument
(like that for linearly itearting a normal measure under $\mathsf{ZFC}$) now
shows that all iterates of $(\mathcal{L}[j],\mu_{j})$ are wellfounded and the
ultrapowers satisfy Los’ theorem, so $(\mathcal{L}[j],\mu_{j})$ is iterable.

Let
$\mathscr{L}^{\prime}[j^{\prime}]=\mathrm{Ult}_{0}(\mathscr{L}[j],\mu_{j})$
and $\widehat{j}:\mathscr{L}[j]\to\mathscr{L}^{\prime}[j^{\prime}]$ be the
ultrapower map. Note that $\mathscr{L}[j]$ and $\mathscr{L}$ have the same
functions $f:V_{\lambda+1}\to L_{\Theta}(V_{\lambda+1})$. So the two
ultrapowers ($\mathrm{Ult}_{0}(\mathscr{L},\mu_{j})$ and
$\mathrm{Ult}_{0}(\mathscr{L}[j],\mu_{j})$) agree on the part computed with
such functions, and in particular

$L_{\Theta}(V_{\lambda+1})=j(L_{\Theta}(V_{\lambda+1}))=\widehat{j}(L_{\Theta}(V_{\lambda+1}))$

and
$j\\!\upharpoonright\\!L_{\Theta}(V_{\lambda+1})=\widehat{j}\\!\upharpoonright\\!L_{\Theta}(V_{\lambda+1})$.
We have
$\mathscr{L}^{\prime}=\widehat{j}(\mathscr{L})=\bigcup_{\alpha\in\mathrm{OR}}\widehat{j}(L_{\alpha}(V_{\lambda+1}))$.
Note that $\mathscr{L}^{\prime}=\mathscr{L}$, but we keep writing
$\mathscr{L}^{\prime}$ for clarity. Let

$k:\mathrm{Ult}_{0}(\mathscr{L},\mu_{j})\to\widehat{j}(\mathscr{L})$

be the natural factor map; that is,

$k([f]^{\mathscr{L},0}_{\mu_{j}})=[f]^{\mathscr{L}[j],0}_{\mu_{j}}=\widehat{j}(f)(j\\!\upharpoonright\\!V_{\lambda}).$

Then (by Los’ theorem) $k$ is fully elementary, and by the agreement of the
ultrapower constructions regarding functions mapping into
$L_{\Theta}(V_{\lambda+1})$, we have $\mathrm{crit}(k)\geq\Theta$. But $k$ is
computed in $\mathscr{L}[j]$, where $V_{\lambda+1}^{\\#}$ does not exist.
Therefore $k=\mathrm{id}$. So all functions $f\in\mathscr{L}[j]$ mapping into
$\mathscr{L}$ are represented mod $\mu_{j}$-measure one by functions
$g\in\mathscr{L}$, so $\mathscr{L}[j]$ is a tight extension of
$\mathscr{L}$.171717 An analogous thing holds for many direct limit systems of
mice, a fact due independently to the second author and Schindler, via the
argument in [18] or in [15]. In the current context, we can use this simpler
“non-existence of $V_{\lambda+1}^{\\#}$” argument instead, which was also
observed independently by Goldberg. By Lemma 3.8, $(\mathscr{L},\mu_{j})$ is
iterable (including Los’ theorem for the ultrapowers constructed by the
iterates etc), and the rest of part 3 also follows.

Part 4: The following should be a standard argument. Let $\eta\leq\lambda$ be
a limit and suppose that $\eta$-$\mathsf{DC}$ holds in $V$. Let
$\mathscr{T}\in\mathscr{L}[j]$ be a tree of height $\leq\eta$. Let
$k=j\\!\upharpoonright\\!\Theta$. Because $\mathscr{L}[j]=\mathscr{L}[k]=L(A)$
for some set $A$, there is a proper class of ordinals $\xi$ such that
$\mathscr{L}[j]\models$“$\xi$ is regular”. Fix some such $\xi>\Theta$ with
$\mathscr{T}\in L_{\xi}(V_{\lambda+1},k)$. Let

$H=\mathrm{Hull}_{\Sigma_{1}}^{L_{\xi}(V_{\lambda+1},k)}(V_{\lambda+1}\cup\\{k,\mathscr{T}\\})$

(this hull is defined as usual (see §1.1), except that we restrict to allowing
only $\Sigma_{1}$ formulas $\varphi$).

Now $\mathscr{L}[j]\models$“$H$ is closed under $\eta$-sequences”. For let
$\left<x_{\alpha}\right>_{\alpha<\eta}\in\mathscr{L}[j]$ with each
$x_{\alpha}H$. Working in $\mathscr{L}[j]$, select for each $\alpha<\eta$ the
least $\Sigma_{1}$ formula $\varphi$ such that for some finite tuple
$\vec{y}\in(V_{\lambda+1}\cup\\{k,\mathscr{T}\\})^{<\omega}$, $x_{\alpha}$ is
the unique $x\in L_{\xi}(V_{\lambda+1},k)$ such that

$L_{\xi}\models\varphi(x,\vec{y}),$

and set $\varphi_{\alpha}=\varphi$. Now working in $V$, where we have
$\eta$-$\mathsf{DC}$, choose a sequence
$\left<\vec{y}_{\alpha}\right>_{\alpha<\eta}$, such that for each
$\alpha<\eta$, $\vec{y}_{\alpha}$ witnesses the choice of $\varphi_{\alpha}$.
Note that $\left<\vec{y}_{\alpha}\right>_{\alpha<\eta}\in\mathscr{L}$. By the
regularity of $\xi$ in $\mathscr{L}[j]$ (and upward absoluteness of
$\Sigma_{1}$ truth) there is $\gamma<\xi$ such that for each $\alpha<\eta$,

$L_{\gamma}\models\varphi_{\alpha}(x_{\alpha},\vec{y}_{\alpha}).$

But then from the parameter
$\left<\varphi_{\alpha},\vec{y}_{\alpha}\right>_{\alpha<\eta}$, we can recover
$\left<x_{\alpha}\right>_{\alpha<\eta}$ in a $\Sigma_{1}$ fashion over
$L_{\xi}(V_{\lambda+1},k)$, by looking for such an ordinal $\gamma$ and
objects in $L_{\gamma}(V_{\lambda+1},k)$. Therefore
$\left<x_{\alpha}\right>_{\alpha<\eta}\in H$.

Now $H\preccurlyeq_{\Sigma_{1}}L_{\xi}(V_{\lambda+1},k)$, since

$L_{\xi}(V_{\lambda+1},k)=\mathrm{Hull}_{\Sigma_{1}}^{L_{\xi}(V_{\lambda+1},k)}(V_{\lambda+1}\cup\xi\cup\\{k\\}).$

In particular, $H$ is extensional. Let $C$ be the transitive collapse of $H$
and $\pi:C\to H$ the uncollapse map. So $\mathscr{L}[j]\models$“$C$ is closed
under $\eta$-sequences”. In $\mathscr{L}$, there is a surjection
$\pi:V_{\lambda+1}\to C$. Let $\pi(\bar{\mathscr{T}})=\mathscr{T}$. Then since
$\mathrm{crit}(\pi)>\lambda$, $\bar{\mathscr{T}}$ is also a tree of height
$\leq\eta$. So by $\eta$-$\mathsf{DC}$ in $V$, there is a maximal branch $b$
through $\mathscr{T}$. But note that $b\in\mathscr{L}\subseteq\mathscr{L}[j]$,
and since $\mathscr{L}[j]\models$“$C$ is closed under $\eta$-sequences”, $b\in
C\models$“$b$ is maximal through $\bar{\mathscr{T}}$”, and it follows that
$\pi(b)$ is a maximal branch through $\mathscr{T}$ in $\mathscr{L}[j]$, as
desired.

The proof for $\mathscr{L}$ instead of $\mathscr{L}[j]$ is essentially the
same, but slightly easier.

∎

##  4 Embedding extensions and the cofinality of $\Theta$

Having proved the main theorem, we now establish some more features of the
model $\mathscr{L}[j]$. We begin with an examination of existence and
uniqueness of extensions of elementary embeddings, and the relationship of
these issues to $\operatorname{cof}(\Theta)$. We carry on using notation as in
the previous section; in particular, $\lambda$ is an even ordinal, and we
write $\mathscr{L}=L(V_{\lambda+1})$ and
$\Theta=\Theta_{V_{\lambda+1}}^{\mathscr{L}}$. However, we don’t assume
$I_{0,\lambda}$ in general. First an observation which follows easily from the
calculations with ultrapowers in the previous section.

######  Lemma 4.1.

We have:

  1. 1.

In $\mathscr{L}$, there is no $\Sigma_{1}$-elementary
$k:L_{\Theta}(V_{\lambda+1})\to L_{\Theta}(V_{\lambda+1})$.

  2. 2.

There is no set-forcing extension of $\mathscr{L}$ with an embedding
$j:\mathscr{L}\to\mathscr{L}$ such that
$j\\!\upharpoonright\\!V_{\lambda}\in\mathscr{L}$.

###### Proof.

Part 1: Letting $\mu_{k}$ be the measure derived from $k$ with seed
$k\\!\upharpoonright\\!V_{\lambda}$, note that $\mathrm{Ult}(V,\mu_{k})$ is
wellfounded and satisfies Los’ theorem as before. But then
$V=L(V_{\lambda+1})=\mathrm{Ult}(V,\mu_{k})$, and the ultrapower map is
definable from the parameter $\mu_{k}$, contradicting Suzuki [19].

Part 2: Let $W$ be a generic extension of $\mathscr{L}$, via forcing
$\mathbb{P}\in\mathscr{L}$, and suppose $W$ has the class elementary
$j:\mathscr{L}\to\mathscr{L}$, $j\neq\mathrm{id}$, and
$j\\!\upharpoonright\\!V_{\lambda}^{\mathscr{L}}\in\mathscr{L}$. Since
$V_{\lambda+1}^{\\#}$ does not exist in $W$, we must have
$j\\!\upharpoonright\\!V_{\lambda}^{\mathscr{L}}\neq\mathrm{id}$. Now $j$ is
determined by
$j\\!\upharpoonright\\!L_{\Theta}(V_{\lambda+1}^{\mathscr{L}})\notin\mathscr{L}$,
by the previous part. But then standard forcing considerations show that
$\mathbb{P}\times\mathbb{P}$ can be used to force the existence of two
distinct embeddings $j_{1},j_{2}:\mathscr{L}\to\mathscr{L}$ such that
$j_{1}\\!\upharpoonright\\!V_{\lambda}^{\mathscr{L}}=j_{2}\\!\upharpoonright\\!V_{\lambda}^{\mathscr{L}}$.
This contradicts the proof of Proposition 3.6. ∎

######  Definition 4.2.

Let $\lambda$ be even. Work in $\mathscr{L}$ and suppose $j:V_{\lambda}\to
V_{\lambda}$ is elementary. Let $\Theta=\Theta_{\lambda+1}$. Then $T_{j}$
denotes the tree of all attempts to build a function $k:\Theta\to\Theta$ such
that $j\cup k$ extends to a $\Sigma_{1}$-elementary map

$\ell:L_{\Theta}(V_{\lambda+1})\to L_{\Theta}(V_{\lambda+1});$

note here that (i) $\Sigma_{1}$-elementarity is guaranteed by
$\Sigma_{0}$-elementarity and ensuring that
$\ell(\mathcal{J}_{\alpha}(V_{\lambda+1}))=\mathcal{J}_{\ell(\alpha)}(V_{\lambda+1})$
for all $\alpha<\Theta$, because we automatically get cofinality in $\Theta$,
and (ii) $\ell$ is uniquely determined by $j\cup k$. Here the nodes in $T_{j}$
simply consist of maps

$k^{\prime}:(\lambda+\alpha\cdot\omega)\to(\lambda+\beta\cdot\omega)$

for some limits $\alpha,\beta<\Theta$, such that $j\cup k^{\prime}$ extends to
a partial map

$\ell^{\prime}:_{p}L_{\Theta}(V_{\lambda+1})\to L_{\Theta}(V_{\lambda+1})$

with domain $L_{\alpha}(V_{\lambda+1})$, and which is $\Sigma_{1}$-elementary
on its domain (with respect to truth in $L_{\Theta}(V_{\lambda+1})$).

Let $T_{j,\alpha}$ be the $\alpha$th derivation of $T_{j}$ given by
iteratively removing nodes $t$ for which there is a bound on the domains of
extensions of $t$. That is, (i) $T_{j,0}=T_{j}$, (ii) given $T_{j,\alpha}$,
then $T_{j,\alpha+1}$ is the set of all $t\in T_{j,\alpha}$ such that for all
$\beta<\Theta$ there is $s\in T_{j,\alpha}$ with
$t=s\\!\upharpoonright\\!\mathrm{dom}(t)$ and $\beta\leq\mathrm{dom}(s)$, and
(iii) $T_{j,\eta}=\bigcap_{\alpha<\eta}T_{j,\alpha}$ for limit $\eta$. Let
$T_{j,\infty}=\bigcap_{\alpha\in\mathrm{OR}}T_{j,\alpha}$.

######  Lemma 4.3.

Adopt notation as above. Working in $V$, we have:

  1. 1.

Branches through $T_{j,\infty}$ with domain $\Theta$ correspond exactly to
branches through $T_{j}$ with domain $\Theta$, which correspond exactly to
$\Sigma_{1}$-elementary maps $k:L_{\Theta}(V_{\lambda+1})\to
L_{\Theta}(V_{\lambda+1})$ extending $j$, which correspond exactly to
$\Sigma_{1}$-elementary maps $V_{\lambda+2}^{\mathscr{L}}\to
V_{\lambda+2}^{\mathscr{L}}$ extending $j$.

  2. 2.

Therefore $\mathscr{L}$ has no branch through $T_{j,\infty}$ or $T_{j}$ of
length $\Theta$.

  3. 3.

If $T_{j,\infty}\neq\emptyset$ then for every $t\in T_{j,\infty}$ and every
$\alpha<\Theta$, there are $s_{1},s_{2}\in T_{j,\infty}$ with $t\subseteq
s_{1},s_{2}$ and $\alpha\leq\mathrm{dom}(s_{1}),\mathrm{dom}(s_{2})$ and
$s_{1}\not\subseteq s_{2}\not\subseteq s_{1}$.

  4. 4.

If $T_{j,\infty}\neq\emptyset$ and $\operatorname{cof}(\Theta)=\omega$ then
there are at least continuum many pairwise distinct $\Sigma_{1}$-elementary
maps $k:V_{\lambda+2}^{\mathscr{L}}\to V_{\lambda+2}^{\mathscr{L}}$ extending
$j$; this holds in particular if $V_{\lambda+1}^{\\#}$ exists.

###### Proof.

Part 1: Most of this is clear, but to see that any $\Sigma_{1}$-elementary
$k:V_{\lambda+2}^{\mathscr{L}}\to V_{\lambda+2}^{\mathscr{L}}$ extends to a
$\Sigma_{1}$-elementary

$k^{\prime}:L_{\Theta}(V_{\lambda+1})\to L_{\Theta}(V_{\lambda+1}),$

we need to see that wellfoundedness is appropriately definable. But if $<^{*}$
is a pre-linear order on $V_{\lambda+1}$ which is illfounded, then there note
that the wellfounded part of $<^{*}$ has ordertype ${<\Theta}$, and so its
wellfounded part can be computed in a
$\Delta_{1}^{V_{\lambda+2}^{\mathscr{L}}}$ fashion from $<^{*}$. So $k$
preserves wellfoundedness of pre-linear orders, which is enough.

Part 3: The existence of at least one such $s_{1}$ follows immediately from
the definitions. The perfectness of $T_{j,\infty}$ follows from the fact that
$T_{j,\infty}\in\mathscr{L}$, but $\mathscr{L}$ has no branch of length
$\Theta$.

Part 4: Fix a strictly increasing cofinal function $f:\omega\to\Theta$ such
that

$L_{f(n)}(V_{\lambda+1})=\mathrm{Hull}^{L_{f(n)}(V_{\lambda+1})}(V_{\lambda+1})$

for each $n<\omega$. Let $T^{\prime}$ be the tree of of attempts to build a
function

$k:\mathrm{rg}(f)\to\Theta,$

such that $j\cup k$ extends to a $\Sigma_{1}$-elementary

$\ell:L_{\Theta}(V_{\lambda+1})\to L_{\Theta}(V_{\lambda+1}).$

Note that $j\cup k$ determines $\ell$, because
$\ell\\!\upharpoonright\\!L_{f(n)}(V_{\lambda+1})$ is determined by $k(f(n))$
and $j\\!\upharpoonright\\!V_{\lambda+1}$.

Let $T^{\prime\prime}$ be the set of nodes $t\in T^{\prime}$ such that there
is $s\in T_{j,\infty}$ with $t=s\\!\upharpoonright\\!\mathrm{dom}(t)$. Then
note that $T^{\prime\prime}\neq\emptyset$, $T^{\prime\prime}$ is perfect (for
every $t\in T^{\prime\prime}$ there are $s_{1},s_{2}\in T^{\prime\prime}$ with
$t\subseteq s_{1},s_{2}$ but $s_{1}\not\subseteq s_{2}\not\subseteq s_{1}$),
and infinite branches through $T^{\prime\prime}$ correspond exactly to
$\Sigma_{1}$-elementary embeddings $V_{\lambda+2}^{\mathscr{L}}\to
V_{\lambda+2}^{\mathscr{L}}$. But the set of nodes in $T^{\prime\prime}$ is
wellorderable. So $[T^{\prime\prime}]\neq\emptyset$, and in fact,
$T^{\prime\prime}$ has at least continuum many infinite branches. ∎

######  Theorem 4.4.

Let $j$ be a proper $I_{0,\lambda}$-embedding. Then
$T_{j\\!\upharpoonright\\!V_{\lambda},\infty}\neq\emptyset$, and in fact,
$j\\!\upharpoonright\\!\Theta$ gives a cofinal branch. Moreover, in
$\mathscr{L}[j]$ we have:

  1. 1.

Every $\Sigma_{1}$-elementary $k:V_{\lambda+2}^{\mathscr{L}}\to
V_{\lambda+2}^{\mathscr{L}}$ extends uniquely to a fully elementary
$k^{\prime}:\mathscr{L}\to\mathscr{L}$ and there is a unique pair
$(\widehat{k},\widetilde{j})$ such that

$\widehat{k}:\mathscr{L}[j]\to\mathscr{L}[\widetilde{j}],$

is elementary and $k\subseteq\widehat{k}$; moreover,

$\widehat{k}(j)=\bigcup_{\bar{j}\in\mathscr{L}\text{ and }\bar{j}\subseteq
j}k^{\prime}(\bar{j});$

and $k^{\prime},\widehat{k}$ are just the ultrapower maps inuced by $\mu_{k}$,
and $k^{\prime}\subseteq\widehat{k}$.

  2. 2.

For every $j^{\prime}:V_{\lambda}\to V_{\lambda}$, there is at most one
extension of $j^{\prime}$ to a $\Sigma_{1}$-elementary
$k^{\prime}:V_{\lambda+2}^{\mathscr{L}}\to V_{\lambda+2}^{\mathscr{L}}$.

###### Proof.

For the existence/uniqueness of extensions of $\Sigma_{1}$-elementary

$k:V_{\lambda+2}^{\mathscr{L}}\to V_{\lambda+2}^{\mathscr{L}}$

and description in terms of the ultrapower (in $\mathscr{L}[j]$) argue as in
the proof of Theorem 3.9(3). Note here that by Lemma 4.3, such $k$ are
equivalent to $\Sigma_{1}$-elementary

$k^{\prime}:L_{\Theta}(V_{\lambda+1})\to L_{\Theta}(V_{\lambda+1}).$

The rest is then clear using Lemmas 4.3 and 3.3. By Lemma 3.3, we get the
uniqueness of the extensions in $\mathscr{L}[j]$. ∎

We now prove a fact which is reminiscent of the Zipper Lemma; of course the
main case we are thinking about is $X=V_{\lambda+1}$:

######  Theorem 4.5.

Let $X$ be a transitive set with $\operatorname{rank}(X)\subseteq X$ (that is,
$\eta\subseteq X\subseteq V_{\eta}$ for some $\eta\in\mathrm{OR}$, so
$\eta=\operatorname{rank}(X)$). Let

$\theta=\Theta^{L(X)}_{X}=\sup\left\\{\alpha\in\mathrm{OR}\bigm{|}\exists\pi\in
L(X)\ [\pi:X\to\alpha\text{ is surjective}]\right\\}.$

Let $j_{i}:L_{\theta}(X)\to L_{\theta}(X)$ be $\Sigma_{1}$-elementary, for
$i=0,1$, with $j_{i}(X)=X$ and
$j_{0}\\!\upharpoonright\\!X=j_{1}\\!\upharpoonright\\!X$, but $j_{0}\neq
j_{1}$.

  1. 1.

There are cofinally many $\gamma<\theta$ such that
$L_{\gamma}(X)=\mathrm{Hull}^{L_{\gamma}(X)}(X\cup\\{X\\})$.

  2. 2.

$\mathrm{rg}(j_{0})\cap\mathrm{rg}(j_{1})$ is bounded in $L_{\theta}(X)$; in
fact, letting $\alpha<\theta$ be least such that $j_{0}(\alpha)\neq
j_{1}(\alpha)$, we have

$(j_{0}``\theta)\cap(j_{1}``\theta)=j_{0}``\alpha=j_{1}``\alpha.$

  3. 3.

If $j_{0}\\!\upharpoonright\\!X\in L(X)$ then
$\operatorname{cof}(\theta)=\omega$ (in $V$).

###### Proof.

Part 1: This is by a standard condensation argument; here it is: First note
that $\theta$ is the least $\theta^{\prime}\in\mathrm{OR}$ with
$\mathcal{P}(X)\cap L(X)\subseteq L_{\theta^{\prime}}(X)$. So fixing
$A\in\mathcal{P}(X)\cap L(X)$, it suffices to find some $\gamma$ as advertised
with $A\in L_{\gamma}(X)$. Now

$L(X)=\mathrm{Hull}_{\Sigma_{1}}^{L(X)}(X\cup\\{X\\}\cup\mathrm{OR}).$

So let $\alpha<\beta\in\mathrm{OR}$ with $A$ being $\Sigma_{1}$-definable over
$L_{\beta}(X)$ from parameters in $X\cup\\{X,\alpha\\}$. Let

$H=\mathrm{Hull}_{\Sigma_{1}}^{L_{\beta}(X)}(X\cup\\{X,\alpha\\})$

and $C$ be the transitive collapse. Then $C=L_{\gamma}(X)$ for some
$\gamma<\theta$, and $A\in C$, and

$C\models\text{``There is an ordinal }\alpha^{\prime}\text{ such that
}V=\mathrm{Hull}_{\Sigma_{1}}^{V}(X\cup\\{X\\}\cup\\{\alpha^{\prime}\\})\text{''.}$

But then the least such $\alpha^{\prime}$ is definable over $C$ from the
parameter $X$, and therefore $C=\mathrm{Hull}^{C}(X\cup\\{X\\})$.

Part 2: We may assume $j_{0}(\alpha)<j_{1}(\alpha)$. Therefore $\sup
j_{1}``\alpha=\sup j_{0}``\alpha\leq j_{0}(\alpha)<j_{1}(\alpha)$, so
$j_{0}(\alpha)\in\mathrm{rg}(j_{0})\backslash\mathrm{rg}(j_{1})$.

Suppose $j_{0}(\alpha)<\beta<\theta$ and
$\beta\in\mathrm{rg}(j_{0})\cap\mathrm{rg}(j_{1})$. Then the least $\xi>\beta$
with

$L_{\xi}(X)=\mathrm{Hull}^{L_{\xi}(X)}(X\cup\\{X\\})$

is also in $\mathrm{rg}(j_{0})\cap\mathrm{rg}(j_{1})$. But then note that

$\mathrm{rg}(j_{0})\cap
L_{\xi}(X)=\mathrm{Hull}^{L_{\xi}(X)}((j_{i}``X)\cup\\{X\\})=\mathrm{rg}(j_{1})\cap
L_{\xi}(X),$

for $i=0,1$, and therefore $j_{0}(\alpha)\in\mathrm{rg}(j_{1})$,
contradiction.

Part 3: Suppose $j_{i}\\!\upharpoonright\\!X\in L(X)$. Let
$\alpha_{0}=\alpha$, and given $\alpha_{n}$, let
$\alpha_{n+1}=\max(j_{0}(\alpha_{n}),j_{1}(\alpha_{n}))$. Notice by induction
that $\alpha_{n+1}>\alpha_{n}$ for each $n<\omega$. Let
$\gamma=\sup_{n<\omega}\alpha_{n}$; we claim that $\gamma=\theta$. For if
$\gamma<\theta$ then because $j_{i}\\!\upharpoonright\\!X\in L(X)$, and by
part 1 and arguing as in the proof of part 2, we get
$j_{0}\\!\upharpoonright\\!\gamma\in\mathscr{L}$ and
$j_{1}\\!\upharpoonright\\!\gamma\in\mathscr{L}$. But
$\left<\alpha_{n}\right>_{n<\omega}$ can be computed from
$j_{0}\\!\upharpoonright\\!\gamma$ and $j_{1}\\!\upharpoonright\\!\gamma$, so
it is in $L(X)$. But then $j_{0},j_{1}$ are both continuous at $\gamma$, so
$j_{0}(\gamma)=\gamma=j_{1}(\gamma)$, contradicting part 2. ∎

So we know that if $\operatorname{cof}(\Theta)=\omega$ and $j$ is proper then
there are continuum many distinct extensions of
$j\\!\upharpoonright\\!V_{\lambda+1}$ to a $\Sigma_{1}$-elementary
$k:L_{\Theta}(V_{\lambda+1})\to L_{\Theta}(V_{\lambda+1})$, but only one of
these, $j\\!\upharpoonright\\!L_{\Theta}(V_{\lambda+1})$, extends to an
elementary $\mathscr{L}\to\mathscr{L}$. This is the situation in particular if
$V_{\lambda+1}^{\\#}$ exists. If $\operatorname{cof}(\Theta)>\omega$, however,
the situation is very different: by the previous theorem, if
$j_{0},j_{1}:L_{\Theta}(V_{\lambda+1})\to L_{\Theta}(V_{\lambda+1})$ are
$\Sigma_{1}$-elementary and
$j_{0}\\!\upharpoonright\\!V_{\lambda}=j_{1}\\!\upharpoonright\\!V_{\lambda}$
then $j_{0}=j_{1}$. Moreover:

######  Theorem 4.6.

Suppose $k:L_{\Theta}(V_{\lambda+1})\to L_{\Theta}(V_{\lambda+1})$ is
$\Sigma_{1}$-elementary and $\operatorname{cof}(\Theta)>\omega$. Then $k$
extends uniquely to a proper $j:\mathscr{L}\to\mathscr{L}$.

###### Proof.

Uniqueness is by Proposition 3.6. For existence, of course, we use the
ultrapower map $j:\mathscr{L}\to U=\mathrm{Ult}_{0}(\mathscr{L},\mu_{k})$.
This ultrapower satisfies Los’ theorem as usual, so we just need to see it is
wellfounded. So suppose not. Let $\eta\in\mathrm{OR}$ be such that
$\mathrm{Ult}_{0}(L_{\eta}(V_{\lambda+1}),\mu_{k})$ is illfounded. Let
$M=L_{\eta}(V_{\lambda+1})$. Then in fact,
$\mathscr{O}=\mathrm{Ult}_{M}(\eta,\mu_{k})$ is illfounded, where this denotes
the ultrapower of $\eta$ formed with functions $f:V_{\lambda+1}\to\eta$ where
$f\in M$. For we can map $U$ into $\mathscr{O}$ by sending $[f]$ to
$[\operatorname{rank}\circ f]$, noting that if $[f]\in^{U}[g]$ then
$[\operatorname{rank}\circ f]<^{\mathscr{O}}[\operatorname{rank}\circ g]$.
When necessary, we write $[f]^{\eta,M}_{\mu}$ for the element of $\mathscr{O}$
represented by $f$. We write $\mathrm{illfp}(\mathscr{O})$ for the illfounded
part of $\mathscr{O}$. Note $\mathscr{O}$ and $\mathrm{illfp}(\mathscr{O})$
are computed in $V$, where we have $\mu_{k}$, but we do not assume they are
computed in $\mathscr{L}$.

We will mimic the usual proof of linear iterability, identifying a reasonable
notion of “least” element of $\mathrm{illfp}(\mathscr{O})$, use this to
identify a canonical descending sequence through $\mathscr{O}$, and then show
that we can reflect this into the action of $k$ for a contradiction. Note that
we are arguing without assuming any $\mathsf{AC}$ in $V$. We remark that the
identification of the canonical descending sequence will not require the
assumption that $\operatorname{cof}(\Theta)>\omega$; this only comes up later
in the reflection.

So let $(t_{0},\xi_{0})$ be the lexicographically least pair $(t,\xi)$ such
that $t$ is a term and $\xi<\eta$ and for some $y\in V_{\lambda+1}$, we have
$t^{M}(y,\xi)$ is some $f:V_{\lambda+1}\to\eta$ in
$\mathrm{illfp}(\mathscr{O})$. (The minimality of $(t_{0},\xi_{0})$, is
computed in $V$.) Let

$H_{0}=\mathrm{Hull}^{M}(V_{\lambda+1}\cup\\{\xi_{0}\\}),$

so $H_{0}\preccurlyeq M$. Let $C_{0}$ be the transitive collapse of $H_{0}$
and $\pi_{0}:C_{0}\to M$ the uncollapse. So
$H_{0},C_{0},\pi_{0}\in\mathscr{L}$, and $C_{0}\in L_{\Theta}(V_{\lambda+1})$.
Let $\pi_{0}(\bar{\xi}_{0})=\xi_{0}$. Note
$\mathrm{crit}(\pi_{0})=\Theta^{C_{0}}=\Theta\cap H_{0}$ and
$\pi_{0}(\Theta^{C_{0}})=\Theta$. Let
$\mathscr{O}_{0}=\mathrm{Ult}_{0}(C_{0},\mu_{k}\cap C_{0})$. Since
$\mu_{k}\cap C_{0}\in\mathscr{L}$, we have $\mathscr{O}_{0}\in\mathscr{L}$,
and note that $\mathscr{O}_{0}$ is wellfounded, because we can embed it into
$\mathrm{OR}(k(C_{0}))$ (mapping $[f]\mapsto
k(f)(k\\!\upharpoonright\\!V_{\lambda})$). So we identify $\mathscr{O}_{0}$
with its ordertype. Let $\gamma_{0}$ be the least $\gamma<\mathscr{O}_{0}$
such that

$\exists y\in V_{\lambda+1}\
\left(\gamma=[t_{0}^{C_{0}}(\bar{\xi}_{0},y)]^{C_{0},0}_{\mu_{k}\cap
C_{0}}\text{ and
}[t_{0}^{M}(\xi_{0},y)]^{\eta,M}_{\mu_{k}}\in\mathrm{illfp}(\mathscr{O})\right).$

Let $Y_{0}$ be the set of all such $y$. So for any such parameters
$y,y^{\prime}$, we have

$[t_{0}^{C_{0}}(\bar{\xi}_{0},y)]^{C_{0},0}_{\mu_{k}\cap
C_{0}}=\gamma_{0}=[t_{0}^{C_{0}}(\bar{\xi}_{0},y^{\prime})]^{C_{0},0}_{\mu_{k}\cap
C_{0}}$

and

$[t_{0}^{M}(\xi_{0},y)]^{\eta,M}_{\mu_{k}}=[t_{0}^{M}(\xi_{0},y^{\prime})]^{\eta,M}_{\mu_{k}}\in\mathrm{illfp}(\mathscr{O}).$

Now choose $(t_{1},\xi_{1})$ as for $(t_{0},\xi_{0})$, except we also require
that

$[t^{M}(\xi,y)]^{\eta,M}_{\mu_{k}}<^{\mathscr{O}}[t_{0}^{M}(\xi_{0},y^{\prime})]^{\eta,M}_{\mu_{k}}\text{
for any/all }y^{\prime}\in Y_{0}.$

Then define $H_{1}=\mathrm{Hull}^{M}(V_{\lambda+1}\cup\\{\xi_{0},\xi_{1}\\})$,
and define $C_{1},\pi_{1},\mathscr{O_{1}}$ like before. Let
$\pi_{1}(\bar{\xi}^{1}_{0},\bar{\xi}^{1}_{1})=(\xi_{0},\xi_{1})$. Let
$\gamma_{1}$ be the least $\gamma<\mathscr{O}_{1}$ such that there is $y\in
V_{\lambda+1}$ such that

  1. –

$\gamma=[t_{1}^{C_{1}}(\bar{\xi}^{1}_{1},y)]^{C_{1},0}_{\mu_{k}\cap C_{1}}$,

  2. –

$[t_{1}^{M}(\xi_{1},y)]^{\eta,M}_{\mu_{k}}\in\mathrm{illfp}(\mathscr{O})$ and

  3. –

$[t_{1}^{M}(\xi_{1},y)]^{\eta,M}_{\mu_{k}}<[t_{0}^{M}(\xi_{0},y^{\prime})]^{\eta,M}_{\mu_{k}}\text{
for any/all }y^{\prime}\in Y_{0}$.

Let $Y_{1}$ be the set of all such $y$. Etc through all finite stages. So
letting

$\gamma^{\mathscr{O}}_{n}=[t_{n}^{M}(\xi_{n},y)]^{\eta,M}_{\mu_{k}}\text{ for
any/all }y\in Y_{n},$

we have $\gamma_{n+1}^{\mathscr{O}}<^{\mathscr{O}}\gamma_{n}^{\mathscr{O}}$
for all $n<\omega$.

Now let
$H=\mathrm{Hull}^{M}(V_{\lambda+1}\cup\\{\xi_{0},\xi_{1},\ldots\\})=\bigcup_{n<\omega}H_{n}$.
We don’t immediately seem to know that $H\in\mathscr{L}$. But still,
$H\preccurlyeq M$ and in $V$ we can form the transitive collapse $C$, and let
$\pi:C\to M$ be the uncollapse. Then $C=L_{\mathrm{OR}^{C}}(V_{\lambda+1})$,
so $C\in\mathscr{L}$. And note $\Theta^{C}=\sup_{n<\omega}\Theta^{C_{n}}$, and
since $\operatorname{cof}(\Theta)>\omega$, we have $\Theta^{C}<\Theta$ (this
is the one key point where we need this assumption). But there are cofinally
many $\alpha<\Theta$ such that $L_{\alpha}(V_{\lambda+1})$ is its own hull of
$V_{\lambda+1}$, and since $C\models$“$\Theta^{C}=\Theta_{V_{\lambda+1}}$”,
there is no such $\alpha$ in $[\Theta^{C},\mathrm{OR}^{C})$. Therefore
$\mathrm{OR}^{C}<\Theta$.

Now $\mathrm{Ult}_{C}(\mathrm{OR}^{C},\mu_{k}\cap C)$ is illfounded by
construction, but like before, we can embed this ultrapower into
$\mathrm{OR}(k(C))$, a contradiction. ∎

Does
$\mathsf{ZF}+I_{0,\lambda}+\operatorname{cof}(\Theta^{\mathscr{L}}_{V_{\lambda+1}})=\omega$
imply the existence of $V_{\lambda+1}^{\\#}$? Similarly, does this theory
together with $\mathsf{AC}$ yield $V_{\lambda+1}^{\\#}$? (Having $\Theta$
singular does routinely imply $\mathcal{P}(V_{\lambda+1})\not\subseteq
L(V_{\lambda+1})$.) It seems natural to try to arrange that
$\operatorname{cof}(\Theta)=\omega$ by forcing over $\mathscr{L}[j]$, without
changing $V_{\lambda+1}$.

##  5
$\mathscr{L}_{\omega}[j_{\omega}]=\mathrm{HOD}^{\mathscr{L}}(\mathscr{L}_{\omega})$
is a ground of $\mathscr{L}$

Much work in inner model theory has been oriented around the analysis of the
$\mathrm{HOD}$ of determinacy models in terms of hod mice or strategy mice,
such as $M_{\infty}[\Sigma]$, for an appropriate direct limit of mice
$M_{\infty}$ and iteration strategy $\Sigma$. (A related strategy mouse,
$M_{1}[\Sigma]$, was already mentioned in the sketch of the main proof,
earlier in the paper.) There has also been analogous analyses of the
$\mathrm{HOD}$ of certain generic extensions of mice. Here we will prove an
analogue, showing that
$\mathrm{HOD}^{\mathscr{L}}(M_{\omega})=M_{\omega}[j_{\omega}]$, and hence
$\mathrm{HOD}^{\mathscr{L}}\subseteq M_{\omega}[j_{\omega}]$ and
$M_{\omega}[j_{\omega}]$ is closed under ordinal definability in
$\mathscr{L}$. The arguments are mostly straightforward adaptations of the
usual ones to our context, and there is such an adaptation in [16]. We assume
$\mathsf{ZF}$, $\lambda$ is even, $I_{0,\lambda}$, $j$ is proper, and fix the
usual notation.

######  Definition 5.1.

Let $x\in\mathscr{L}$. We say that $x$ is _eventually stable_ iff there is
$n<\omega$ such that $j_{n}(x)=x$ (and hence $j_{m}(x)=x$ for all
$m\in[n,\omega)$). We say that $x$ is _hereditarily eventually stable_ (_hes_)
iff every $y\in\mathrm{trancl}(\\{x\\})$ is eventually stable.

We now extend the earlier $*$-map to all eventually stable $x$: given such an
$x$ and $s\in\vec{\Gamma}$ with $x\in H^{s}$, let

$x^{*}=\lim_{n\to\omega}\pi^{j\\!\upharpoonright\\!V_{\lambda},s}_{n\omega}(x)=\lim_{m\to\omega}j_{m\omega}(x),$

so $x^{*}\in\mathscr{L}_{\omega}$.

######  Lemma 5.2.

$\mathscr{L}$ can define the notions _eventually stable_ , _hes_ , and the map
$x\mapsto x^{*}$ (with domain the eventually stable $x$), from the parameter
$j_{n}\\!\upharpoonright\\!V_{\lambda}$, uniformly in $n$.

###### Proof.

A set $x\in\mathscr{L}$ is eventually stable iff there is
$(s,m)\in\mathscr{P}^{j_{n}\\!\upharpoonright\\!V_{\lambda}}$ such that $x\in
H^{s}$ and

$\pi^{j_{n}\\!\upharpoonright\\!V_{\lambda},s}_{m\ell}(x)=x\text{ for all
}\ell\in[m,\omega).$

The map $x\mapsto x^{*}$ is then clearly definable. ∎

Recall
$j_{\omega,\omega+\omega}:\mathscr{L}_{\omega}\to\mathscr{L}_{\omega,\omega+\omega}$
is the iteration map.

######  Definition 5.3.

Define
$\widehat{j}_{\omega,\omega+\omega}:\mathscr{L}_{\omega}[j_{\omega}]\to\mathscr{L}_{\omega+\omega}[j_{\omega+\omega}]$
as the unique elementary extension of $j_{\omega,\omega+\omega}$; by Theorem
3.9, this makes sense and is the iteration map.

######  Lemma 5.4.

Let $x\in\mathscr{L}$. Then $x\in\mathscr{L}_{\omega}[j_{\omega}]$ iff $x$ is
hereditarily eventually stable, and moreover, if
$x\in\mathscr{L}_{\omega}[j_{\omega}]$ then
$\widehat{j}_{\omega,\omega+\omega}(x)=x^{*}$.

###### Proof.

Let $x\in\mathscr{L}_{\omega}$. Then $x$ is hes, because if
$x\in\mathrm{rg}(j_{n})$ then $j_{n}(x)=x$ (we can fix $s\in\vec{\Gamma}$ and
$\bar{x}\in H^{s}$, and so $x=\pi^{s}_{n\omega}(\bar{x})$, and since this fact
is preserved by $j_{n}$, we get $j_{n}(x)=x$). Also if $\alpha\in\mathrm{OR}$,
note that $j_{\omega}\\!\upharpoonright\\!\alpha$ is eventually stable. It
follows that $x$ is hes. We now show that
$x^{*}=\widehat{j}_{\omega,\omega+\omega}(x)$. Let $y\in
V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}$ and $\eta\in\mathrm{OR}$ and
$\varphi$ be a formula such that

$\mathscr{L}_{\omega}[j_{\omega}]\models\text{``}x\text{ is the unique
}x^{\prime}\text{ such that
}\varphi(x^{\prime},y,\eta,j_{\omega}\\!\upharpoonright\\!\Theta)\text{''}.$

Let $n<\omega$ be such that $y\in\mathrm{rg}(j_{n\omega})$ and
$j_{n}(\eta)=\eta$. Then note that $j_{n}(x)=x$ and $j_{n}(y)=y$, and letting
$k=j_{n}\\!\upharpoonright\\!\lambda$, we have ($\mathscr{L}=\mathscr{L}_{n}$
and)

$\mathscr{L}_{n}\models\text{``}x=\text{ unique
}x^{\prime}\in(\widetilde{\mathscr{L}}_{\omega}[\widetilde{j}_{\omega}])^{k}\text{
s.t.~{}}(\widetilde{\mathscr{L}}_{\omega}[\widetilde{j}_{\omega}])^{k}\models\varphi(x^{\prime},y,\eta,(\widetilde{j}_{\omega})^{k}\\!\upharpoonright\\!\Theta)\text{
'' },$

where “s.t.” means “such that” and $(\widetilde{\mathscr{L}}_{\omega})^{k}$
means the version of $\mathscr{L}_{\omega}$ given by iterating $k$, and
$(\widetilde{\mathscr{L}}_{\omega}[\widetilde{j}_{\omega}])^{k}$ likewise (as
computed in $\mathscr{L}=\mathscr{L}_{n}$ here; so in this case it happens
that these are just $\mathscr{L}_{\omega}$ and
$\mathscr{L}_{\omega}[j_{\omega}]$, but the point is that we are referring to
the definitions of these classes from the parameter $k$). So letting
$\ell=j_{\omega}\\!\upharpoonright\\!V_{\lambda_{\omega}}$,

$\mathscr{L}_{\omega}\models\text{``}x^{*}=\text{ unique
}x^{\prime}\in(\widetilde{\mathscr{L}}_{\omega}[\widetilde{j}_{\omega}])^{\ell}\text{
s.t.~{}}(\widetilde{\mathscr{L}}_{\omega}[\widetilde{j}_{\omega}])^{\ell}\models\varphi(x^{\prime},y^{*},\eta^{*},(\widetilde{j}_{\omega})_{\ell}\\!\upharpoonright\\!\Theta)\text{''}$

(as $\Theta^{*}=\Theta$). But $\widehat{j}_{\omega,\omega+\omega}$ extends
$j_{\omega,\omega+\omega}$ and is elementary, and we know that
$j_{\omega,\omega+\omega}(\eta)=\eta^{*}$, and it is easy to see that
$j_{\omega,\omega+\omega}(y)=y^{*}$, and note that
$\widehat{j}_{\omega,\omega+\omega}(j_{\omega}\\!\upharpoonright\\!\Theta)=j_{\omega+\omega}\\!\upharpoonright\\!\Theta$,
so by elementarity of $\widehat{j}_{\omega,\omega+\omega}$, we get
$\widehat{j}_{\omega,\omega+\omega}(x)=x^{*}$.

We now prove by induction on rank that every hes $x$ is in
$\mathscr{L}_{\omega}[j_{\omega}]$. So fix such an $x$ with
$x\subseteq\mathscr{L}_{\omega}[j_{\omega}]$. Then
$x^{*}\in\mathscr{L}_{\omega}$, so $x^{*}\in\mathscr{L}_{\omega}[j_{\omega}]$.
But $x\subseteq\mathscr{L}_{\omega}[j_{\omega}]$, and since $*$ agrees with
$\widehat{j}_{\omega,\omega+\omega}$ over $\mathscr{L}_{\omega}[j_{\omega}]$,
using this map and $x^{*}$, $\mathscr{L}_{\omega}[j_{\omega}]$ can compute
$x$. ∎

In the following theorem, we write $\mathrm{OD}(X)$ for the class of all $x$
such that $x$ is definable from (finitely many) parameters in $\mathrm{OR}\cup
X$; note that we officially do not allow $X$ as a predicate here, but in the
case below, that will make no difference. We then define $\mathrm{HOD}(X)$
from $\mathrm{OD}(X)$ just as $\mathrm{HOD}$ is defined from $\mathrm{OD}$.

######  Theorem 5.5.

$\mathrm{HOD}^{\mathscr{L}}(\mathscr{L}_{\omega})=\mathrm{HOD}^{\mathscr{L}}(\mathscr{L}_{\omega}[j_{\omega}])=\mathscr{L}_{\omega}[j_{\omega}]$.

###### Proof.

We first show that
$\mathrm{HOD}^{\mathscr{L}}(\mathscr{L}_{\omega}[j_{\omega}])\subseteq\mathscr{L}_{\omega}[j_{\omega}]$.
Proceeding again by induction on rank, let
$A\in\mathrm{HOD}^{\mathscr{L}}(\mathscr{L}_{\omega}[j_{\omega}])$ be such
that $A\subseteq\mathscr{L}_{\omega}[j_{\omega}]$; it suffices to see that
$A\in\mathscr{L}_{\omega}[j_{\omega}]$. Let
$p\in\mathscr{L}_{\omega}[j_{\omega}]$ and $\varphi$ be a formula such that
for $x\in\mathscr{L}_{\omega}[j_{\omega}]$, we have

$x\in A\iff\mathscr{L}\models\varphi(p,x).$

Then since both $p,x$ are hes, we get

$x\in
A\iff\mathscr{L}_{\omega}\models\varphi(p^{*},x^{*})\iff\mathscr{L}_{\omega}\models\varphi(\widehat{j}_{\omega,\omega+\omega}(p),\widehat{j}_{\omega,\omega+\omega}(x)),$

so $A\in\mathscr{L}_{\omega}[j_{\omega}]$.

So to prove the theorem, it just suffices to see that
$j_{\omega}\\!\upharpoonright\\!\Theta$ is definable over $\mathscr{L}$ from
the parameter
$(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}},j_{\omega}\\!\upharpoonright\\!V^{\mathscr{L}_{\omega}}_{\lambda_{\omega}})$.
But in $\mathscr{L}$,
$j_{\omega}\\!\upharpoonright\\!L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})$
is the unique $\Sigma_{1}$-elementary

$k:L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})\to
L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})$

extending $j_{\omega}\\!\upharpoonright\\!V_{\lambda_{\omega}+1}$, by Theorem
4.5.181818An earlier draft of this paper, on arxiv.org, used the following
argument here instead: observe that the desired embedding is the unique
embedding $k$ extending $j\\!\upharpoonright\\!V_{\lambda_{\omega}+1}$ such
that $\mathrm{Ult}_{0}(\mathscr{L}_{\omega},\mu_{k})$ is wellfounded, because
otherwise we can argue as for Proposition 3.6 for a contradiction. ∎

Using the preceding result, we next observe that
$\mathscr{L}_{\omega}[j_{\omega}]$ is a (set-)ground for $\mathscr{L}$, via
Vopenka forcing $\mathrm{Vop}$ for adding $j_{0\omega}``V_{\lambda}$
generically to $\mathscr{L}_{\omega}[j_{\omega}]$. Moreover, we will analyze
aspects of this forcing.

######  Definition 5.6.

Work in $\mathscr{L}$. Let $\widetilde{\mathrm{Vop}}$ be the partial order
whose elements are the non-empty sets
$A\subseteq\mathcal{P}(V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}})$ which are
$\mathrm{OD}(\mathscr{L}_{\omega})$, with ordering $\widetilde{\leq}$ being
$\subseteq$. Let $\mathrm{Vop}^{\prime}$ be the following partial order. The
conditions are tuples $p=(a,\gamma,\eta,\varphi)$ with $a\in
V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}$, $\gamma<\eta\in\mathrm{OR}$
with $\lambda_{\omega}+1<\eta$, and $\varphi$ a formula. Given such a tuple
$p$, let

$A_{p}=A_{(a,\gamma,\eta,\varphi)}=\\{x\subseteq
V_{\lambda_{\omega}}^{\mathcal{L}_{\omega}}\bigm{|}\mathscr{L}|\eta\models\varphi(x,a,\gamma,V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})\\},$

so $A_{p}\in\widetilde{\mathrm{Vop}}$. The ordering of $\mathrm{Vop}^{\prime}$
is then $p\leq^{\prime}q$ iff $A_{p}\subseteq A_{q}$. So if
$\mathrm{Vop}^{\prime}/\equiv$ is isomorphic to $\widetilde{\mathrm{Vop}}$,
where $\equiv$ is the usual equivalence relation ($p\equiv q$ iff
$p\leq^{\prime}q\leq^{\prime}p$). Finally let $\mathrm{Vop}$ be the
restriction of $\mathrm{Vop}^{\prime}$ to tuples $p\in
L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})$, and
$\leq^{\mathrm{Vop}}$ its order.

######  Lemma 5.7.

We have:

  1. 1.

$\mathrm{Vop}/\equiv$ is isomorphic to $\widetilde{\mathrm{Vop}}$.

  2. 2.

$\mathrm{Vop}$ is definable from parameters over
$(L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}),j_{\omega}\\!\upharpoonright\\!\Theta)$.

  3. 3.

The set of pairs $(y,p)\in
V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}\times\mathrm{Vop}$ such that $y\in
x$ for every $x\in A_{p}$, is definable over
$(L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}),j_{\omega}\\!\upharpoonright\\!\Theta)$.

  4. 4.

Every antichain of $\mathrm{Vop}$ which is in $\mathscr{L}$ is in
$L_{\alpha}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})$ for some
$\alpha<\Theta$.

###### Proof.

Part 1: Given any $p\in\mathrm{Vop}^{\prime}$, we can take a hull to replace
$p$ with an equivalent condition $q$ below $\Theta$, and note then that $q\in
L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})$. (Note here that
each subset of $V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}$ is coded by an
element of $V_{\lambda+1}$.)

Part 2: Working over
$L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})$, from
$j_{\omega}\\!\upharpoonright\\!V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}$
and the predicate $j_{\omega}\\!\upharpoonright\\!\Theta$, we can compute
$j_{\omega}\\!\upharpoonright\\!L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})$,
and hence
$j_{\omega,\omega+\omega}\\!\upharpoonright\\!L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})$,
by iterating the former embedding. Now for $p,p_{1}\in\mathrm{Vop}$ with
$p=(a,\gamma,\eta,\varphi)$ and
$p_{1}=(a_{1},\gamma_{1},\eta_{1},\varphi_{1})$, we have
$p\leq^{\mathrm{Vop}}p_{1}$ iff $A_{p}\subseteq A_{p_{1}}$ iff
$L_{\Theta}(V_{\lambda+1})\models$“for all $x\subseteq
V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}$,

$L_{\eta}(V_{\lambda+1})\models\varphi(x,a,\gamma,V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})\implies
L_{\eta_{1}}(V_{\lambda+1})\models\varphi_{1}(x,a_{1},\gamma_{1},V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})$

iff $L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})\models$“for all
$x\subseteq(V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}})^{*}$,

$L_{\eta^{*}}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})\models\varphi(x,a^{*},\gamma^{*},(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})^{*})\implies
L_{\eta_{1}^{*}}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})\models\varphi_{1}(x,a_{1}^{*},\gamma_{1}^{*},(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})^{*})\text{''}$

(recalling that we extended $*$ to $\mathscr{L}_{\omega}$, in fact to
$\mathscr{L}_{\omega}[j_{\omega}]$, above). Since $*$ agrees with
$j_{\omega,\omega+\omega}$, this gives the claimed definability of
$\leq^{\mathrm{Vop}}$, assuming the set of conditions of $\mathrm{Vop}$ is
likewise definable, but the latter is similar.

Part 3: This is much like the previous part.

Part 4: Note that if $A\subseteq\mathrm{Vop}$ is an antichain then for all
$p,q\in A$ with $p\neq q$ we have $A_{p}\cap A_{q}=\emptyset$. But then if the
elements of $A$ are constructed unboundedly in
$L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}})$, then
$\mathscr{L}$ would have a surjection from $V_{\lambda+1}$ to $\Theta$, a
contradiction. ∎

Now let $x\subseteq V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}$. (Note that
every such $x$ is in $\mathscr{L}$, since $\mathscr{L}$ has a surjection from
$V_{\lambda}$ onto $V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}$.) We can now
proceed as usual to show that $x$ induces filter $G_{x}$ which is
$(\mathscr{L}_{\omega}[j_{\omega}],\mathrm{Vop})$-generic, with
$x\in\mathscr{L}_{\omega}[j_{\omega}][G_{x}]$. That is, let

$G_{x}=\\{p\in\mathrm{Vop}\bigm{|}x\in A_{p}\\}.$

Then $G_{x}$ is easily a filter. For genericity, let
$D\in\mathscr{L}_{\omega}[j_{\omega}]$, $D\subseteq\mathrm{Vop}$, be dense.
Then note that in $\mathrm{Vop}$ there is a condition $p$ such that
$A_{p}=\bigcup_{q\in D}A_{q}$. So if $A_{p}\subsetneq
V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}$ then there is also $p^{\prime}$
with $A_{p^{\prime}}=V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}\backslash
A_{p}$. But then note that $p^{\prime}$ is incompatible with every $q\in D$, a
contradiction. So $A_{p}=V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}$, so
there is $q\in D$ with $x\in A_{q}$, so $G_{x}\cap D\neq\emptyset$, as
desired.

To see that $x\in\mathscr{L}_{\omega}[j_{\omega}][G_{x}]$, use part 3 of Lemma
5.7.

Now applying this with $x=j_{0\omega}``V_{\lambda}$, note that in
$\mathscr{L}_{\omega}[j_{\omega}][G_{x}]$, we can compute $V_{\lambda}$ and
$j_{0\omega}\\!\upharpoonright\\!V_{\lambda}$, and from these data, given any
$X\subseteq V_{\lambda}$, since $j_{0\omega}(X)\in\mathscr{L}_{\omega}$, we
can then invert and compute $X$. So
$\mathscr{L}_{\omega}[j_{\omega}][G_{x}]=\mathscr{L}$.

Now let $\mathrm{Vop}_{\mathrm{hom}}$ be the restriction of $\mathrm{Vop}$
below the condition $p$, where

$A_{p}=\\{x\subseteq
V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}\bigm{|}V_{\lambda+1}\subseteq
L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}},x)\\},$

noting that $A_{p}$ is appropriately definable in $\mathscr{L}$. Then clearly:

######  Claim.

For every $p\in\mathrm{Vop}_{\mathrm{hom}}$ there is $x\subseteq
V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}$ such that $p\in G_{x}$ and
$\mathscr{L}_{\omega}[j_{\omega}][G_{x}]=\mathscr{L}$.

Therefore, $\mathscr{L}_{\omega}[j_{\omega}]$ can compute the theory of
$\mathscr{L}$ in parameters in $\mathscr{L}_{\omega}[j_{\omega}]$, as it is
just what is forced by $\mathrm{Vop}_{\mathrm{hom}}$. (But we had already
observed that
$\mathrm{HOD}^{\mathscr{L}}(\mathscr{L}_{\omega}[j_{\omega}])=\mathscr{L}_{\omega}[j_{\omega}]$.)

We have proved he following theorem, as witnessed by
$\mathbb{P}=\mathrm{Vop}_{\mathrm{hom}}$:191919Goldberg has also communicated
to the author that $\mathscr{L}_{\omega}[j_{\omega}]$ is also a ground of
$\mathscr{L}$ via a certain Prikry forcing.

######  Theorem 5.8.

$\mathscr{L}_{\omega}[j_{\omega}]$ is a ground of $\mathscr{L}$, via a forcing
$\mathbb{P}$ such that:

  1. 1.

$\mathbb{P}$ is definable from parameters over the structure
$(L_{\Theta}(V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}),j_{\omega}\\!\upharpoonright\\!\Theta)$,

  2. 2.

every antichain of $\mathbb{P}$ in $\mathscr{L}_{\omega}[j_{\omega}]$ is the
surjective image of $V_{\lambda_{\omega}+1}^{\mathscr{L}_{\omega}}$ in
$\mathscr{L}_{\omega}[j_{\omega}]$,

  3. 3.

every antichain of $\mathbb{P}$ in $\mathscr{L}$ is the surjective image of
$V_{\lambda+1}$ in $\mathscr{L}$,

  4. 4.

every condition $p\in\mathbb{P}$ is contained in an
$\mathscr{L}_{\omega}[j_{\omega}]$-generic filter $G$ such that
$\mathscr{L}_{\omega}[j_{\omega}][G]=\mathscr{L}$.

With the broader $\mathrm{Vop}$, we might have sets $x\subseteq
V_{\lambda_{\omega}}^{\mathscr{L}_{\omega}}$ such that
$x\notin\mathscr{L}_{\omega}[j_{\omega}]$ but
$\mathscr{L}_{\omega}[j_{\omega}][G_{x}]\neq\mathscr{L}$. In this case we get

$\mathscr{L}_{\omega}[j_{\omega}][G_{x}]=\mathrm{HOD}^{\mathscr{L}}(\mathscr{L}_{\omega}[j_{\omega}]\cup\\{x\\}),$

by basically the usual calculations. (Note that every element of the model on
the right can be coded by a subset of $\mathscr{L}_{\omega}[j_{\omega}]$;
these all get into $\mathscr{L}_{\omega}[j_{\omega}][G_{x}]$ by the usual
argument.)

Now although
$\mathscr{L}_{\omega}[j_{\omega}]=\mathrm{HOD}^{\mathscr{L}}(\mathscr{L}_{\omega}[j_{\omega}])$:

######  Theorem 5.9.

We have:

  1. 1.

$\mathscr{L}_{\omega}[j_{\omega}]\subsetneq\mathrm{HOD}^{\mathscr{L}[j]}(\mathscr{L}_{\omega}[j_{\omega}])$.

  2. 2.

$\mathcal{P}(\Theta)\cap\mathrm{HOD}^{\mathscr{L}[j]}\not\subseteq\mathscr{L}$.

###### Proof.

Part 1: In $\mathscr{L}[j]$, $\mathscr{L}=L(V_{\lambda+1})$, so
$\mathrm{HOD}^{\mathscr{L}}(\mathscr{L}_{\omega}[j_{\omega}])\subseteq\mathrm{HOD}^{\mathscr{L}[j]}(\mathscr{L}_{\omega}[j_{\omega}])$.
So suppose
$\mathrm{HOD}^{\mathscr{L}[j]}(\mathscr{L}_{\omega}[j_{\omega}])=\mathscr{L}_{\omega}[j_{\omega}]$.
This will contradict part 2 once we have it, but before we proceed to that
part, we sketch an alternate argument for contradiction.

Under the contradictory hypothesis, more Vopenka forcing gives that
$\mathscr{L}[j]$ is a set-generic extension of
$\mathscr{L}_{\omega}[j_{\omega}]$. But $\mathscr{L}_{\omega}[j_{\omega}]$ is
the $\omega$th iterate of $\mathscr{L}[j]$, so we have the elementary
embedding

$j_{0\omega}^{+}:\mathscr{L}[j]\to\mathscr{L}_{\omega}[j_{\omega}],$

which is $\Sigma_{5}$-definable from parameters over $\mathscr{L}[j]$. But
then we can use a standard argument for a contradiction: Working in
$\mathscr{L}_{\omega}[j_{\omega}]$, let $\kappa_{0}\in\mathrm{OR}$ be least
such that for some forcing $\mathbb{P}$, $\mathbb{P}$ forces “there is a
$\Sigma_{1}$-elementary embedding $k:V^{\mathbb{P}}\to V$ which is
$\Sigma_{5}$-definable from parameters and $\mathrm{crit}(k)=\kappa_{0}$”.
Then $\kappa_{0}$ is outright definable over
$\mathscr{L}_{\omega}[j_{\omega}]$, but taking a witnessing generic and $k$,
then $k$ is actually fully elementary by [12, ***?], so
$\kappa\in\mathrm{rg}(k)$, so $\kappa\neq\mathrm{crit}(k)$, contradiction.

Part 2: Work in $\mathscr{L}[j]$. Let $X$ be the set of all $\alpha<\Theta$
such that $k(\alpha)=\alpha$ for all $I_{0,\lambda}$-embeddings $k$. We claim
that $X$ witnesses the theorem.

First, the definition we have just given (inside $\mathscr{L}[j]$) shows that
$X\in\mathrm{HOD}^{\mathscr{L}[j]}$ (in fact $X$ is definable without
parameters, since $\lambda$ is definable without parameters).

Now $X$ is unbounded in $\Theta$. If $V_{\lambda+1}^{\\#}$ exists (in $V$)
then this is by Proposition 3.6. But otherwise, working in $\mathscr{L}[j]$,
let $\Lambda$ be the class of all ordinals which are fixed by all
$I_{0,\lambda}$-embeddings $k$. By the non-existence of $V_{\lambda+1}^{\\#}$
in $\mathscr{L}[j]$,
$\mathrm{Hull}^{\mathscr{L}}(V_{\lambda+1}\cup\Lambda)=\mathscr{L}$. Moreover,
$\mathrm{Hull}^{\mathscr{L}}(\Lambda)$ is unbounded in $\Theta$. For given
$\alpha<\Theta$, let $s\in[\Lambda]^{<\omega}$ and $n<\omega$ be such that

$H=\mathrm{Hull}_{\Sigma_{n}}^{\mathscr{L}}(V_{\lambda+1}\cup\\{s\\})$

includes some $\beta\in(\alpha,\Theta)$. Note that $\sup(H\cap\Theta)<\Theta$
and this sup is in $\mathrm{Hull}^{\mathscr{L}}(\Lambda)$, which suffices. But
clearly $\Lambda=\mathrm{Hull}^{\mathscr{L}}(\Lambda)\cap\mathrm{OR}$, and
$X=\Lambda\cap\Theta$, so we are done.

But $X\notin\mathscr{L}$, because if we had $X\in\mathscr{L}$, then we easily
get $j\\!\upharpoonright\\!L_{\Theta}(V_{\lambda+1})\in\mathscr{L}$, which is
false. That is, note there are unboundedly many $\alpha<\Theta$ such that
$\alpha\in X$ and

$L_{\alpha}(V_{\lambda+1})=\mathrm{Hull}^{L_{\alpha}(V_{\lambda+1})}(V_{\lambda+1}),$

and so $j\\!\upharpoonright\\!L_{\alpha}(V_{\lambda+1})$ is determined by
$j\\!\upharpoonright\\!V_{\lambda+1}\in\mathscr{L}$ and that
$j(\alpha)=\alpha$. ∎

##  6 Sharps at even and odd levels

Since $\mathscr{L}[j]\models$“$j:L(V_{\lambda+1})\to L(V_{\lambda+1})$ and
$V_{\lambda+2}\subseteq L(V_{\lambda+1})$” (with $\lambda$ even as before,
etc), we trivially have that $\mathscr{L}[j]\models$“$j:L(V_{\lambda+2})\to
L(V_{\lambda+2})$” (but this does not hold with $\lambda+3$ replacing
$\lambda+2$, since $j\\!\upharpoonright\\!\Theta$ is coded by an element of
$V_{\lambda+3}$). So we have the following fact:

######  Theorem 6.1.

If $\mathsf{ZF}+$“$\lambda$ is an even ordinal and $j:L(V_{\lambda+2})\to
L(V_{\lambda+2})$ is elementary with $\mathrm{crit}(j)<\lambda$” is
consistent, then it does not imply the existence of $V_{\lambda+1}^{\\#}$.

We show now that at odd levels, this is completely otherwise. The proof is
motivated by a proof, to appear in [16],202020At the time of writing, this
result is not in the version of [16] on arxiv.org, but will appear in the next
version. which shows that if $j:V\to V$ then $M_{n}^{\\#}(X)$ exists for every
set $X$. Goldberg [8] has other sharp existence results, including [8,
Corollary 6.11], by which if $\lambda$ is even and $k:V_{\lambda+3}\to
V_{\lambda+3}$ is $\Sigma_{1}$-elementary then $A^{\\#}$ exists for every
$A\in V_{\lambda+2}$ (note that by the following, if in fact
$j:L(V_{\lambda+3})\to L(V_{\lambda+3})$ then $A^{\\#}$ exists for every $A\in
V_{\lambda+3}$):

######  Theorem 6.2.

Assume $\mathsf{ZF}+I_{0,\lambda}$ where $\lambda$ is even. Then $A^{\\#}$
exists for every $A\in V_{\lambda+1}$.

Note here that that by Theorem 3.9, if $\mathsf{ZF}+I_{0,\lambda}$ is
consistent then it does not imply that $V_{\lambda+1}^{\\#}$ exists, so the
result above is in a sense optimal. But of course one might also ask whether
there are natural classes of sets $A\subseteq V_{\lambda+1}$ which do not code
all elements of $V_{\lambda+1}$, and which for which
$\mathsf{ZF}+I_{0,\lambda}$ does prove the existence of $A^{\\#}$.

###### Proof.

Let $j$ be an $I_{0,\lambda}$-embedding and $A\subseteq V_{\lambda}$. We will
first prove that $j(A)^{\\#}$ exists, and then deduce from this that $A^{\\#}$
exists.

If $\lambda$ is a limit, let $\mu$ be the $V_{\lambda}$-extender derived from
$j$, and otherwise let $\mu$ be the measure derived from $j$ with seed
$j\\!\upharpoonright\\!V_{\lambda-2}$; so $\mu\in V_{\lambda+1}$. By [9], we
have $\mathrm{Ult}(V_{\lambda},\mu)=V_{\lambda}$ and
$j\\!\upharpoonright\\!V_{\lambda}$ is the ultrapower map, and
$\mathrm{Ult}(V_{\lambda+1},\mu)\subsetneq V_{\lambda+1}$, but
$j\\!\upharpoonright\\!V_{\lambda+1}$ is still the ultrapower map associated
to the latter ultrapower. Therefore

$\mathrm{Ult}((V_{\lambda},A),\mu)=(V_{\lambda},j(A)).$

Let $M=L(V_{\lambda},A)$. We form the internal ultrapower
$\mathrm{Ult}_{0}(M,\mu)$; that is, we only use functions in $M$ to form the
ultrapower.

######  Claim.

The ultrapower satisfies Los’ theorem.

###### Proof.

We consider the case that $\lambda$ is a successor first. Let $f\in M$ with
$f:\mathscr{E}(V_{\lambda-2})\to M$ and suppose

$\forall^{*}_{\mu}k\ [M\models\exists x\varphi(x,f(k))].$

Then by the elementarity of $j$, we can fix $x\in j(M)$ such that

$j(M)=L(V_{\lambda},j(A))\models\varphi(x,j(f)(j\\!\upharpoonright\\!V_{\lambda-2})).$

Let $y\in V_{\lambda}$ and $t$ be a term be such that

$j(M)\models x=t(y,j(f)(j\\!\upharpoonright\\!V_{\lambda}),j(A)).$

The function $f_{y}:\mathscr{E}(V_{\lambda-2})\to V_{\lambda}$ defined

$f_{y}(k)=(k^{+})^{-1}``y,$

(where $k^{+}$ is the canonical extension of $k$; see Remark 2.1) is such that
$f_{y}\in V_{\lambda}$ and $[f_{y}]^{V_{\lambda}}_{\mu}=y$. Now define the
function $g\in M$, $g:\mathscr{E}(V_{\lambda-2})\to M$, by

$g(k)=t(f_{y}(k),f(k),A).$

Then $j(g)(j\\!\upharpoonright\\!V_{\lambda-2})=x$, and therefore

$\forall^{*}_{\mu}k\ [M\models\varphi(g(k),f(k))],$

as desired.

Now suppose instead that $\lambda$ is a limit. We use the theory of extenders
under $\mathsf{ZF}$ developed in [16]. Let
$a\in\left<V_{\lambda}\right>^{<\omega}$ and $f\in M$ with
$f:\left<V_{\lambda}\right>^{<\omega}\to M$ be such that

$\forall^{*}_{\mu_{a}}k\ [M\models\exists x\varphi(x,f(k))].$

Then by elementarity and since
$j(M)\models$“$V=\mathrm{HOD}(V_{\lambda},j(A))$”, we get again some $x\in
j(M)$ such that

$j(M)\models\varphi(x,j(f)(a))$

and some $y\in V_{\lambda}$ term $t$ such that

$j(M)\models x=t(y,j(f)(a),j(A)).$

By enlarging $y$, we can assume that $a\subseteq
y\in\left<V_{\lambda}\right>^{<\omega}$. In $M$, let
$g:\left<V_{\lambda}\right>^{<\omega}\to M$ be defined

$g(k)=t(k,f^{ay}(k),A).$

Then by elementarity, $j(g)(y)=x$ and

$\forall^{*}_{\mu_{y}}k\ [M\models\varphi(g(k),f^{ay}(k))],$

so we are done. ∎

In particular, $U=\mathrm{Ult}(M,\mu)$ is extensional, and letting
$i=i^{M}_{\mu}$, the ultrapower map, $i:M\to U$ is elementary. We also have
the factor map

$k:U\to j(M),$

defined as usual by

$k([f]^{M}_{\mu})=j(f)(j\\!\upharpoonright\\!V_{\lambda})$

in the successor case and in the limit case by

$k([a,f]^{M}_{\mu})=j(f)(a).$

By Los’ theorem, $k$ is elementary. Therefore $U$ is wellfounded, and
moreover, note that $V_{\lambda}\subseteq U$ and
$k\\!\upharpoonright\\!V_{\lambda}=\mathrm{id}$, and $k\circ
i=j\\!\upharpoonright\\!M$. Therefore

$U=L(V_{\lambda},j(A))=j(M).$

So $k:j(M)\to j(M)$ and either $k=\mathrm{id}$ or $\mathrm{crit}(k)>\lambda$.

Now if $\mathrm{crit}(k)>\lambda$ then we have $(V_{\lambda},j(A))^{\\#}$, so
suppose $k=\mathrm{id}$. We have $k\circ i=j\\!\upharpoonright\\!M$, and
therefore $i\\!\upharpoonright\\!\mathrm{OR}=k\circ
i\\!\upharpoonright\\!\mathrm{OR}=j\\!\upharpoonright\\!\mathrm{OR}$ by our
assumption. But $i$ is computed inside $L(V_{\lambda+1})$, because $\mu\in
V_{\lambda+1}$. And $j\\!\upharpoonright\\!V_{\lambda+1}$ is also computed in
$L(V_{\lambda+1})$, because it is the ultrapower map associated to
$\mathrm{Ult}(V_{\lambda+1},\mu)$ (see [9]). But since
$L(V_{\lambda+1})\models$“$V=\mathrm{HOD}(V_{\lambda+1})$”, $j$ is determined
by $j\\!\upharpoonright\\!(V_{\lambda+1}\cup\mathrm{OR})$. Therefore $j$ is
definable over $L(V_{\lambda+1})$ from the parameter $\mu$, contradicting
Suzuki [19].

So we have $(V_{\lambda},j(A))^{\\#}$. Now $M=L(V_{\lambda},A)$. Let

$\ell=i^{M}_{\mu}:L(V_{\lambda},A)\to L(V_{\lambda},j(A))$

be the ultrapower map (so
$\ell\\!\upharpoonright\\!V_{\lambda}=j\\!\upharpoonright\\!V_{\lambda}$ and
$\ell(A)=j(A)$). Let $\Lambda$ be a proper class of fixed points of $\ell$
which are Silver indiscernibles for $L(V_{\lambda},j(A))$. Let
$\iota=\min(\Lambda)$ and

$H=\mathrm{Hull}^{M}(V_{\lambda}\cup\\{A\\}\cup\Lambda\backslash\\{\iota\\}).$

Note that $H\preccurlyeq M$, $\iota\notin H$, but
$V_{\lambda}\cup\\{\lambda,A\\}\subseteq H$, so $M$ is the transitive collapse
of $H$, and letting $\pi:M\cong H$ be the uncollapse map, then $\pi:M\to M$ is
elementary with $\lambda<\mathrm{crit}(\pi)$, so we are done. ∎

##  7 Questions

Some natural questions:

  1. 1.

What is the precise consistency strength of $\mathsf{ZF}+$“there is an
elementary $j:V_{\lambda+2}\to V_{\lambda+2}$”? Is it equiconsistent with some
extension of $\mathsf{ZFC}$?

  2. 2.