\documentclass[12pt]{article}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{diagram}
\newcommand{\ga}{\alpha}
\newcommand{\gb}{\beta}
\renewcommand{\gg}{\gamma}
\newcommand{\gd}{\delta}
\newcommand{\gep}{\epsilon}
\newcommand{\gz}{\zeta}
\newcommand{\gee}{\eta}
\newcommand{\gth}{\theta}
\newcommand{\gi}{\iota}
\newcommand{\gk}{\kappa}
\newcommand{\gl}{\lambda}
\newcommand{\gm}{\mu}
\newcommand{\gn}{\nu}
\newcommand{\gx}{\xi}
\newcommand{\gom}{\omicron}
\newcommand{\gp}{\pi}
\newcommand{\gr}{\rho}
\newcommand{\gs}{\sigma}
\newcommand{\gt}{\tau}
\newcommand{\gu}{\upsilon}
\newcommand{\gph}{\phi}
\newcommand{\gch}{\chi}
\newcommand{\gps}{\psi}
\newcommand{\go}{\omega}
\newcommand{\gA}{A}
\newcommand{\gB}{B}
\newcommand{\gG}{\Gamma}
\newcommand{\gD}{\Delta}
\newcommand{\gEp}{E}
\newcommand{\gZ}{Z}
\newcommand{\gEe}{H}
\newcommand{\gTh}{\Theta}
\newcommand{\gI}{I}
\newcommand{\gK}{K}
\newcommand{\gL}{\Lambda}
\newcommand{\gM}{M}
\newcommand{\gN}{N}
\newcommand{\gX}{\Xi}
\newcommand{\gOm}{O}
\newcommand{\gP}{\Pi}
\newcommand{\gR}{P}
\newcommand{\gS}{\Sigma}
\newcommand{\gT}{T}
\newcommand{\gU}{\Upsilon}
\newcommand{\gPh}{\Phi}
\newcommand{\gCh}{X}
\newcommand{\gPs}{\Psi}
\newcommand{\gO}{\Omega}
\newcommand{\bA}{{\bf A}}
\newcommand{\bB}{{\bf B}}
\newcommand{\bG}{\boldGamma}
\newcommand{\bD}{\boldDelta}
\newcommand{\bEp}{{\bf E}}
\newcommand{\bZ}{{\bf Z}}
\newcommand{\bEe}{{\bf H}}
\newcommand{\bTh}{\boldTheta}
\newcommand{\bI}{{\bf I}}
\newcommand{\bK}{{\bf K}}
\newcommand{\bL}{{\bf L}}
\newcommand{\bM}{{\bf M}}
\newcommand{\bN}{{\bf N}}
\newcommand{\bX}{\boldXi}
\newcommand{\bOm}{{\bf O}}
\newcommand{\bP}{\boldPi}
\newcommand{\bR}{{\bf P}}
\newcommand{\bS}{\boldSigma}
\newcommand{\bT}{{\bf T}}
\newcommand{\bU}{\boldUpsilon}
\newcommand{\bPh}{\boldPhi}
\newcommand{\bCh}{{\bf X}}
\newcommand{\bPs}{\boldPsi}
\newcommand{\bO}{\boldOmega}
\newcommand{\rest}{\restriction}
\newcommand{\la}{\langle}
\newcommand{\ra}{\rangle}
\newcommand{\ov}{\overline}
\newcommand{\add}{{\rm Add}}
\newcommand{\K}{{\cal K}}
\newcommand{\U}{{\cal U}}
%
% Hebrew letters
%
\newcommand{\ha}{\aleph}
\newcommand{\hb}{\beth}
\newcommand{\hg}{\gimel}
\newcommand{\hd}{\daleth}
%
% basic set theory constructions
%
\newcommand{\setof}[2]{{\{\; #1 \; \vert \; #2 \; \} } }
\newcommand{\seq}[1]{{\langle #1 \rangle} }
\newcommand{\card}[1]{{\vert #1 \vert} }
\newcommand{\ot}[1]{\hbox{o.t.($#1$)}}
\newcommand{\forces}{\Vdash}
\newcommand{\decides}{\parallel}
\newcommand{\ndecides}{\nparallel}
\renewcommand{\models}{\vDash}
\newcommand{\powerset}{{\cal P}}
\newcommand{\bool}{{\bf b} }%
%
% stuff for use inside math formulae
%
\newcommand{\dom}{{\rm dom}}
\newcommand{\rge}{{\rm rge}}
\newcommand{\crit}{{\rm crit}}
\renewcommand{\top}{{\rm top}}
\newcommand{\supp}{{\rm supp}}
\newcommand{\support}{{\rm support}}
\newcommand{\cf}{{\rm cf}}
\newcommand{\lh}{{\rm lh}}
\newcommand{\lp}{{\rm lp}}
\newcommand{\up}{{\rm up}}
\newcommand{\FF}{{\mathbb F}}
\newcommand{\FP}{{\mathbb P}}
\newcommand{\FQ}{{\mathbb Q}}
\newcommand{\FR}{{\mathbb R}}
\newcommand{\FS}{{\mathbb S}}
\newcommand{\FT}{{\mathbb T}}
\newcommand{\implies}{\Longrightarrow}
\newcommand{\commtriangle}[6]
{
\medskip
\[
\setlength{\dgARROWLENGTH}{6.0em}
\begin{diagram}
\node{#1} \arrow[2]{e,t}{#6} \arrow{se,b}{#4} \node[2]{#3} \\
\node[2]{#2} \arrow{ne,r}{#5}
\end{diagram}
\]
\medskip
}
%
% This picture tells you what order to put the arguments in
%
%
%
%
% #6
% #1 --------- #3
% \ /
% \#4 / #5
% \ /
% #2/
%
\newtheorem{theorem}{Theorem}
\newtheorem{definition}{Definition}[section]
\newtheorem{remark}[definition]{Remark}
\newtheorem{fact}[definition]{Fact}
\newtheorem{lemma}[definition]{Lemma}
\newtheorem{claim}[definition]{Claim}
\newtheorem{conjecture}{Conjecture}
\newenvironment{proof}{\noindent{\bf
Proof:}}{\nopagebreak\mbox{}\newline\makebox[\textwidth]{\hfill$\square$}
\par\bigskip}
\newenvironment{sketch}{\noindent{\bf
Sketch of Proof:}}{\nopagebreak\mbox{}\newline
\makebox[\textwidth]{\hfill$\square$}\par\bigskip}
\newenvironment{pf}{\indent{${}$}}{\nopagebreak\mbox{}\newline
\makebox[\textwidth]{\hfill$\square$}\par\bigskip}
\newcommand{\lra}{\longrightarrow}
\setlength{\topmargin}{-0.62in}
\setlength{\textheight}{9.10in}
\setlength{\oddsidemargin}{-0.15in}
\setlength{\textwidth}{6.95in}
\setlength{\parindent}{1.5em}
%\setcounter{section}{+1}
%\setcounter{theorem}{-1}
% IndWC.tex
% The following macros are a selection from Joel's general math
% macros used in the document below
%
\def\tlt{\triangleleft}
\def\k{\kappa}
\def\a{\alpha}
\def\b{\beta}
\def\d{\delta}
\def\s{\sigma}
\def\t{\tau}
\def\l{\lambda}
\def\lted{{{\leq}\d}}
\def\ltk{{{<}\k}}
%
% Arthur, in the next two macro definitions, use blackboard bold for
% \bm. Latex uses a different name I think.
%
\def\P{{\mathbb P}}
\def\Q{{\mathbb Q}}
\def\Qdot{\dot\Q}
\def\Pforces{\forces_{\P}}
\def\of{{\subseteq}}
%\def\card#1{\left|#1\right|}
\def\boolval#1{\mathopen{\lbrack\!\lbrack}\,#1\,\mathclose{\rbrack\!
\rbrack}}
\def\restrict{\mathbin{\mathchoice{\hbox{\am\char'26}}{\hbox{\am\char'
26}}{\hbox{\eightam\char'26}}{\hbox{\sixam\char'26}}}}
\def\colon{:}
\def\st{\mid}
\def\set#1{\{\,{#1}\,\}}
\def\th{{\hbox{\fiverm th}}}
\def\muchgt{>>}
\def\cof{\mathop{\rm cof}\nolimits}
\def\iff{\mathrel{\leftrightarrow}}
\def\intersect{\cap}
\def\minus{\setminus}
\def\Union{\bigcup}
\def\union{\bigcup}
\def\and{\mathrel{\kern1pt\&\kern1pt}}
\def\image{\mathbin{\hbox{\tt\char'42}}}
\def\elesub{\prec}
\def\iso{\cong}
\def\<#1>{\langle\,#1\,\rangle}
\def\ot{\mathop{\rm ot}\nolimits}
%
% ------------------------------------------------------------------------------
%
\title{The Consistency of $V = {\rm HOD}$ with Level by Level Equivalence
\thanks{2010 Mathematics Subject Classifications:
03E35, 03E55.}
\thanks{Keywords: Supercompact cardinal, strongly compact cardinal,
level by level equivalence between strong
compactness and supercompactness, lottery sum,
Ground Axiom (GA), diamond, square, HOD.}}
\author{Arthur W.~Apter\\
% \thanks{The
% author's research was partially
% supported by PSC-CUNY grants.}\\
Department of Mathematics\\
Baruch College of CUNY\\
New York, New York 10010 USA\\
and\\
The CUNY Graduate Center, Mathematics\\
365 Fifth Avenue\\
New York, New York 10016 USA\\
http://faculty.baruch.cuny.edu/aapter\\
awapter@alum.mit.edu}
%\date{March 15, 2017}\date{April 9, 2017}\date{April 30, 2017}
%\date{May 3, 2017}
\date{May 5, 2017}
\begin{document}
\maketitle
\begin{abstract}
We construct two models showing
the relative consistency of $V = {\rm HOD}$ with the
level by level equivalence between strong compactness and supercompactness.
In the first model, various versions of the combinatorial principles
$\square$ and $\diamondsuit$ hold. %along with level by level equivalence.
In the second model, the Ground Axiom (GA) holds.
%along with level by level equivalence.
\end{abstract}
\baselineskip=24pt
\section{Introduction and Preliminaries}\label{s1}
In \cite{AC08}, the following theorem was proven.
\begin{theorem}\label{t1}
Let
$V \models ``$ZFC + GCH + $\K \neq
\emptyset$ is the class of
supercompact cardinals''.
There is then a partial ordering
$\FP \subseteq V$ such that
$V^\FP \models ``$ZFC + GCH + $\K$ is
the class of supercompact cardinals +
Level by level equivalence
between strong compactness and
supercompactness holds''.
In $V^\FP$, $\square^S_\gg$ holds
for every infinite cardinal $\gg$,
where $S = {\rm Safe}(\gg)$.
In addition, in $V^\FP$, $\diamondsuit_\mu$
holds for every $\mu$ which is
inaccessible or the successor of
a singular cardinal, and
$\diamondsuit^+_\mu$ holds for every
$\mu$ which is the successor
of a regular cardinal.
\end{theorem}
Quoting from \cite{AC08},
in terminology used by Woodin,
this theorem
%to describe the main theorem of \cite{AS97a},
can be classified as an
``inner model theorem proven via forcing.''
This is since the witnessing model %constructed
satisfies pleasant properties
one usually associates with an
inner model, namely {GCH and many instances of square and diamond,}
along with a property one might
perhaps expect if a ``nice'' inner model
containing supercompact
cardinals ever were to be
constructed (see \cite{Wo17} for a discussion of this topic), namely
level by level equivalence
between strong compactness
and supercompactness.
Theorem \ref{t1} can also be considered as a part of S$.$ Friedman's ``outer
model program'', as first described in \cite{F06}.
The purpose of this paper is to prove two theorems
in which we create via forcing models
for the level by level equivalence between strong compactness and supercompactness
satisfying both $V = {\rm HOD}$ and additional inner model properties.
In the first of these theorems, we prove a generalized version of
Theorem \ref{t1} in which level by level equivalence
between strong compactness and supercompactness and various versions
of diamond and square are true.
For the second of these theorems, we recall that {\em the Ground Axiom (GA)},
introduced in \cite{FHR, R07}, is the assertion that the set-theoretic universe
$V$ is not a forcing extension of any inner model $W \subseteq V$ by
nontrivial set forcing $\FP \in W$.
Any canonical inner model, e.g., $L$, $L_{\cal U}$ for $\gk$ a
measurable cardinal and $\U$ a normal measure over $\gk$,
$L[\vec E]$ for $\vec E$ a coherent sequence of extenders, etc.,
satisfies GA.
%In the second of these theorems,
In our second theorem, we construct a model in which both level by
level equivalence between strong compactness and supercompactness and
%the Ground Axiom (GA) introduced in \cite{FHR, R07}
GA are true.
%, but the additional inner model property $V = {\rm HOD}$ holds as well.
%and the Ground Axiom (GA) hold as well.
Specifically, we will prove the following.
\begin{theorem}\label{t2}
Let
$V \models ``$ZFC + GCH + $\K \neq
\emptyset$ is the class of
supercompact cardinals''.
There is then a partial ordering
$\FP \subseteq V$ such that
$V^\FP \models ``$ZFC + GCH + $\K$ is
the class of supercompact cardinals +
Level by level equivalence
between strong compactness and
supercompactness holds + $V = {\rm HOD}$''.
In $V^\FP$, $\square^S_\gg$ holds
for every infinite cardinal $\gg$,
where $S = {\rm Safe}(\gg)$.
In addition, in $V^\FP$, $\diamondsuit_\mu$
holds for every regular cardinal $\mu$, and
$\diamondsuit^+_\mu$ holds for every
$\mu$ such that $\mu = \gl^+$, $\gl$ is regular,
but $\gl$ is not the successor of a singular cardinal.
%$\mu$ such that $\mu = \gl^{++}$ where $\gl$ is regular.
%Finally, the Ground Axiom GA holds in $V^\FP$.
%$\mu$ which is the successor
%of a regular cardinal which is not the successor of a singular cardinal.
\end{theorem}
\begin{theorem}\label{t2a}
Let
$V \models ``$ZFC + GCH + $\K \neq
\emptyset$ is the class of
supercompact cardinals''.
Assume further that in $V$, there is a proper class of measurable cardinals.
There is then a partial ordering
$\FP \subseteq V$ such that
$V^\FP \models ``$ZFC + GCH + $\K$ is
the class of supercompact cardinals''.
In $V^\FP$, there is a proper class of measurable cardinals.
In addition, in $V^\FP$,
level by level equivalence
between strong compactness and
supercompactness, $V = {\rm HOD}$, and GA
%the Ground Axiom (GA)
all hold. %in $V^\FP$. %holds as well.
%Finally, the Ground Axiom GA holds in $V^\FP$.
\end{theorem}
We take this opportunity to make a few additional remarks concerning
Theorems \ref{t2} and \ref{t2a}.
Although the model witnessing the conclusions of Theorem \ref{t2} satisfies the
same instances of the kind of square that Theorem \ref{t1} does,
it does not satisfy exactly the same instances of the different versions of diamond.
This is due to the coding partial ordering that we use to force
$V = {\rm HOD}$, which will decide generically
%where $\diamondsuit^+_\mu$ holds
where $\diamondsuit^*_\mu$ holds
or fails whenever $\mu$ is the double successor of a singular cardinal.
We will be able to infer that $\diamondsuit_\mu$ holds for every successor cardinal
$\mu$ by Shelah's celebrated result of \cite{Sh10}, since our
forcing will preserve GCH.
The coding oracle employed to force $V = {\rm HOD}$
and GA in Theorem \ref{t2a} requires
a proper class of measurable cardinals, which is the reason for this
additional hypothesis.
Also, Theorem \ref{t2a} is a generalization of \cite[Theorem 4.2]{AF11},
where a model containing a proper class of supercompact
cardinals in which GCH, $V = {\rm HOD}$, and GA all hold is built via forcing.
We conclude Section \ref{s1} with a discussion of some preliminary material.
Suppose $V$ is a model of ZFC
in which for all regular cardinals
$\gk < \gl$, $\gk$ is $\gl$ strongly
compact iff $\gk$ is $\gl$ supercompact,
except possibly if $\gk$ is a measurable limit
of cardinals $\gd$ which are $\gl$ supercompact.
Such a universe will be said to
witness {\em level by level
equivalence between strong
compactness and supercompactness}.
For brevity, we will henceforth abbreviate this as just
{\em level by level equivalence}.
%Any model witnessing level by
%level equivalence between strong
%compactness and supercompactness
%also witnesses the Kimchi-Magidor
%property \cite{KM} that the classes
%of strongly compact and supercompact
%cardinals coincide precisely,
%except at measurable limit points.
The exception
is provided by a theorem of Menas \cite{Me},
who showed that if $\gk$ is a measurable limit
of cardinals $\gd$ which are $\gl$ strongly
compact, then $\gk$ is $\gl$ strongly compact
but need not be $\gl$ supercompact.
%Models in which level by level
%equivalence between strong compactness
%and supercompactness holds nontrivially
%were first constructed in \cite{AS97a}.
%We take this opportunity to
%elaborate a bit more on the notion of
%level by level equivalence between strong
%compactness and supercompactness.
Any model of ZFC with this property
also witnesses the Kimchi-Magidor
property \cite{KM} that the classes
of strongly compact and supercompact
cardinals coincide precisely,
except at measurable limit points.
Models in which GCH and level by level
equivalence between strong compactness
and supercompactness hold nontrivially
were first constructed by Shelah and the author in \cite{AS97a}.
We presume a basic knowledge
of large cardinals and forcing.
A good reference in this regard is \cite{J}.
When forcing, $q \ge p$ means that
{\em $q$ is stronger than $p$}.
We will have some slight abuses of notation.
In particular,
when $G$ is $V$-generic over $\FP$,
we %abuse notation slightly and
take both $V[G]$ and
$V^\FP$ as being the generic
extension of $V$ by $\FP$.
We will also, from time to time,
confuse terms with the sets
they denote and write
$x$ when we actually mean
$\dot x$ or $\check x$.
%We also %abuse notation slightly by
%occasionally confuse terms with the
%sets they denote, especially for
%ground model sets and variants of the generic object.
For $\ga < \gb$ ordinals, $[\ga, \gb]$, $[\ga, \gb)$, $(\ga, \gb]$, and
%$[\ga, \gb)$ and %$(\ga, \gb]$, $[\ga, \gb]$, and
$(\ga, \gb)$ are as in standard interval notation.
%For any ordinal $\ga$, $\ga'$ is the least inaccessible cardinal
%above $\ga$.
For $\gk < \gl$ regular cardinals,
${\rm Coll}(\gk, \gl)$ is the usual L\'evy collapse
of all cardinals in the half-open interval $(\gk, \gl]$ to $\gk$.
For $\gk$ a regular cardinal and $\gl$ an ordinal,
$\add(\gk, \gl)$ is the
standard partial ordering for adding
$\gl$ many Cohen subsets of $\gk$.
The partial ordering
$\FP$ is {\em $\gk$-directed closed} if
every directed set of conditions
of size less than $\gk$ has
an upper bound.
%For $\gk$ a measurable cardinal, the
%normal measure ${\cal U}$ over $\gk$ has
%{\em trivial Mitchell rank} if for
%$j : V \to M$ the elementary embedding
%generated by ${\cal U}$,
%$M \models ``\gk$ is not measurable''.
%$\FP$ is {\em $\gk$-closed} if every increasing
%chain of members of $\FP$ of length $\gk$ has an upper bound.
%$\FP$ is {\em ${<}\gk$-closed} if $\FP$ is
%$\gd$-closed for every $\gd < \gk$.
%$\FP$ is {\em $\gk$-strategically closed}
%if in the two person game in which the
%players construct an increasing sequence
%$\la p_\ga \mid \ga \le \gk \ra$,
%where player I plays odd stages and
%player II plays even stages,
%player II has a strategy ensuring the game
%can always be continued.
%$\FP$ is {\em ${\prec}\gk$-strategically closed}
%if in the two person game in which the
%players construct an increasing sequence
%$\la p_\ga \mid \ga < \gk \ra$,%
%where player I plays odd stages and
%player II plays even stages,
%player II has a strategy ensuring the game
%can always be continued.
%It therefore follows that
%any partial ordering $\FP$ which is
%$\gk$-directed closed is also
%${\prec }\gk$-strategically closed
%and consequently adds no new subsets of
%any cardinal $\gd < \gk$.
%$\FP$ is {\em ${<}\gk$-strategically closed}
%if $\FP$ is $\gd$-strategically closed
%for every $\gd < \gk$.
%$\FP$ is {\em $(\gk, \infty)$-distributive}
%if the intersection of $\gk$ many
%dense open subsets of $\FP$ is dense open.
%It therefore follows that
%any partial ordering $\FP$ which is
%$\gk$-directed closed is also
%${<}\gk$-strategically closed, and any
%partial ordering which is $\gk$-strategically
%closed is $(\gk, \infty)$-distributive.
%It further
%We assume familiarity with the
%large cardinal notions of
%measurability, strong compactness, and supercompactness.
%Readers are urged to consult \cite{J} for further details.
%We do mention, however, that
%the cardinal $\gk$ is ${<} \gl$
%strongly compact or ${<} \gl$ supercompact if
%$\gk$ is $\gg$ strongly compact or $\gg$
%supercompact for every $\gg < \gl$.
%We do note, however, that
%we will say {\em $\gk$ is supercompact
%up to the inaccessible cardinal $\gl$} if
%$\gk$ is $\gd$ supercompact for every $\gd < \gl$.
We recall for the benefit of readers the
definition given by Hamkins in
\cite[Section 3]{H4} of the lottery sum
of a collection of partial orderings.
If ${\mathfrak A}$ is a collection of partial orderings, then
the {\it lottery sum} is the partial ordering
$\oplus {\mathfrak A} =
\{\la \FP, p \ra \mid \FP \in {\mathfrak A}$
and $p \in \FP\} \cup \{0\}$, ordered with
$0$ below everything and
$\la \FP, p \ra \le \la \FP', p' \ra$ iff
$\FP = \FP'$ and $p \le p'$.
Intuitively, if $G$ is $V$-generic over
$\oplus {\mathfrak A}$, then $G$
first selects an element of
${\mathfrak A}$ (or as Hamkins says in \cite{H4},
``holds a lottery among the posets in
${\mathfrak A}$'') and then
forces with it.\footnote{The terminology
``lottery sum'' is due to Hamkins, although
the concept of the lottery sum of partial
orderings has been around for quite some
time and has been referred to at different
junctures via the names ``disjoint sum of partial
orderings,'' ``side-by-side forcing,'' and
``choosing which partial ordering to force
with generically.''}
A corollary of Hamkins' work of \cite{H03}
on the approximation and cover properties
(which is a generalization of his
gap forcing results found in \cite{H2, H3})
will be employed in the
proofs of Theorems \ref{t2} and \ref{t2a}.
This corollary follows from \cite[Theorems 3, 31, and Corollary 14]{H03}.
We therefore state as a
separate theorem
what is relevant for this paper, along
with some associated terminology,
quoting from \cite{H2, H3, H03}
when appropriate.
Suppose $\FP$ is a partial ordering
which can be written as
$\FQ \ast \dot \FR$, where
$\card{\FQ} \le \gd$,
$\FQ$ is nontrivial, and
$\forces_\FQ ``\dot \FR$ is
%$\gd$-strategically closed''.
$\gd^+$-directed closed''.
In Hamkins' terminology of
\cite{H03}, %\cite{H2, H3},
$\FP$ {\em admits a closure point at $\gd$}.
In Hamkins' terminology of
\cite{H2, H3, H03},
$\FP$ is {\em mild
with respect to a cardinal $\gk$}
iff every set of ordinals $x$ in
$V^\FP$ of size below $\gk$ has
a ``nice'' name $\tau$
in $V$ of size below $\gk$,
i.e., there is a set $y$ in $V$,
$|y| <\gk$, such that any ordinal
forced by a condition in $\FP$
to be in $\tau$ is an element of $y$.
Also, as in the terminology of
\cite{H2, H3, H03} and elsewhere,
an embedding
$j : V \to \ov M$ is
{\em amenable to $V$} when
$j \rest A \in V$ for any
$A \in V$.
The specific corollary of
Hamkins' work from
\cite{H03} %\cite{H2, H3}
we will be using
is then the following.
\begin{theorem}\label{tgf}
%(Hamkins' Gap Forcing Theorem)
{\bf(Hamkins)}
Suppose that $V[G]$ is a generic
extension obtained by forcing with $\FP$
that admits a closure point %gap
at some regular $\gd < \gk$.
Suppose further that
$j: V[G] \to M[j(G)]$ is an elementary embedding
with critical point $\gk$ for which
$M[j(G)] \subseteq V[G]$ and
${M[j(G)]}^\gd \subseteq M[j(G)]$ in $V[G]$.
Then $M \subseteq V$; indeed,
$M = V \cap M[j(G)]$. If the full embedding
$j$ is amenable to $V[G]$, then the
restricted embedding
$j \rest V : V \to M$ is amenable to $V$.
If $j$ is definable from parameters
(such as a measure or extender) in $V[G]$,
then the restricted embedding
$j \rest V$ is definable from the names
of those parameters in $V$.
Finally, if $\FP$ is mild with
respect to $\gk$ and $\gk$ is
$\gl$ strongly compact in $V[G]$
for any $\gl \ge \gk$, then
$\gk$ is $\gl$ strongly compact in $V$.
\end{theorem}
It immediately follows from Theorem \ref{tgf}
that any cardinal $\gk$ which is $\gl$ supercompact
in a generic extension obtained
by forcing that admits a closure point
below $\gk$ (such as at $\go$)
must also be $\gl$ supercompact
in the ground model.
In particular, if $\ov V$ is a generic extension
of $V$ by a partial ordering admitting a closure point
%below the least supercompact cardinal
at $\go$
in which each supercompact cardinal is preserved,
the class of supercompact cardinals in $\ov V$ remains
the same as in $V$.
In addition, it follows from Theorem \ref{tgf} that
if $\FP$ admits a closure point at $\go$, $\FP$ is mild with respect to $\gk$, and
$V^\FP \models ``\gk$ is $\gl$ strongly compact'', then %where $\gl$ is regular'', then
it is also true that
$V \models ``\gk$ is $\gl$ strongly compact''.
%Further, Theorem \ref{tgf} implies that if
%$V^\FP \models ``\gk$ is $\gl$ strongly compact'' ,
%$\FP$ admits a closure point at $\go$, and $\FP$ is mild with respect to $\gk$, then
%$V \models ``\gk$ is $\gg$ strongly compact'' for any ordinal $\gg$ such that
%$V^\FP \models ``\card{\gg} = \gl$''.
%A consequence of Theorem \ref{tgf} is that if
%$\FP$ admits a gap at $\ha_1$ and
%$V^\FP \models ``\varphi(\gk)$'' where
%$\varphi(\gk)$ is either the formula which says
%``$\gk$ is supercompact'' or the formula which says
%``$\gk$ is measurable'', then
%$V \models ``\varphi(\gk)$'' as well.
%In addition, it follows from Theorem \ref{tgf} that
%if $\FP$ admits a gap at $\ha_1$, $\FP$ is mild with respect to $\gk$, and
%$V^\FP \models ``\gk$ is strongly compact'', then
%it is also true that
%$V \models ``\gk$ is strongly compact''. %as well.
%\noindent A consequence of Theorem \ref{tgf} is that if
%$\FP$ admits a gap at $\ha_1$ and %some regular $\gd < \gk$ and
%$V^\FP \models ``\gd$ is measurable'', then
%$V \models ``\gd$ is measurable'' as well.
%In particular, if $\FP$ admits a gap at $\go$, then
%Finally, at several junctures throughout
We end Section \ref{s1}
by stating the definitions of the combinatorial notions we will be using.
Readers may consult \cite{AC08} for additional details,
from which we will feel free to quote verbatim when appropriate.
If $\gk$ is a regular uncountable
cardinal, $\diamondsuit_\gk$ is
the principle stating that
there exists a sequence of sets
$\la S_\ga \mid \ga < \gk \ra$ such that
$S_\ga \subseteq \ga$,
with the additional property that
for every $X \subseteq \gk$,
$\{\ga < \gk \mid X \cap \ga = S_\ga\}$ is
a stationary subset of $\gk$.
We recall that if $\gl$ is an uncountable cardinal
\begin{enumerate}
%\item $\diamondsuit'_{\lambda^+}$ is the assertion that there exists
% a sequence $\langle {\mathcal S}_\alpha: \alpha < \lambda^+ \rangle$
% such that
%\begin{enumerate}
%\item For every $\alpha$, ${\mathcal S}_\alpha$ is a family of subsets
% of $\alpha$ with $\vert {\mathcal S}_\alpha \vert \le \lambda$.
%\item For every $X \subseteq \lambda^+$, the set
% $\{ \alpha < \lambda^+ : X \cap \alpha \in {\mathcal S}_\alpha \}$ is
% stationary in $\alpha$.
%\end{enumerate}
\item $\diamondsuit^*_{\lambda^+}$ is the assertion that there exists
a sequence $\langle {\mathcal S}_\alpha \mid \alpha < \lambda^+ \rangle$
such that
\begin{enumerate}
\item For every $\alpha$, ${\mathcal S}_\alpha$ is a family of subsets
of $\alpha$ with $\vert {\mathcal S}_\alpha \vert \le \lambda$.
\item For every $X \subseteq \lambda^+$, there is $C \subseteq \lambda^+$ a
club set such that
$\forall \alpha \in C \; X \cap \alpha \in {\mathcal S}_\alpha$.
\end{enumerate}
\item $\diamondsuit^+_{\lambda^+}$ is the assertion that there exists
a sequence $\langle {\mathcal S}_\alpha \mid \alpha < \lambda^+ \rangle$
such that
\begin{enumerate}
\item For every $\alpha$, ${\mathcal S}_\alpha$ is a family of subsets
of $\alpha$ with $\vert {\mathcal S}_\alpha \vert \le \lambda$.
\item For every $X \subseteq \lambda^+$, there is $C \subseteq \lambda^+$ a
club set such
$\forall \alpha \in C \; X \cap \alpha, C \cap \alpha \in {\mathcal S}_\alpha$.
\end{enumerate}
\end{enumerate}
%\noindent
We explicitly make the observation that trivially, by their
definitions, $\diamondsuit^+_{\lambda^+} \implies \diamondsuit^*_{\lambda^+}$.
This of course means that if $\diamondsuit^*_{\lambda^+}$ fails, then so does
$\diamondsuit^+_{\lambda^+}$. We will use this explicitly in our coding
and in our proof of Lemma \ref{l3} showing that in our desired generic extension,
$V = {\rm HOD}$.
We give a partial version of square, $\square^S_\gk$
for $\gk$ an uncountable cardinal and $S \subseteq \gk$
a set of regular cardinals, %$\square$
compatible with supercompact
cardinals. {
As was mentioned in \cite[Section 2.1]{AC08},
square sequences of this kind were first shown to be
consistent with supercompactness by Foreman and Magidor
\cite[page 191]{VWS}, using techniques
of Baumgartner. In the notation of Definition \ref{funnysquare}
found immediately below, they
showed that $\square_{\kappa^{+\omega}}^{ \{ \kappa^{+n} \mid n < \omega \}
}$ is consistent with $\kappa$ being supercompact. }
Given a set $S$ of regular cardinals, we denote by ${\rm cof}(S)$
the class of ordinals $\alpha$ such that ${\rm cf}(\alpha) \in S$.
We also let REG stand for the class of regular cardinals.
\begin{definition} \label{funnysquare} Let $\kappa$ be an infinite cardinal and let $S$ be
a set of regular cardinals which are less than or equal to $\kappa$.
Then a {\em $\square_\kappa^S$-sequence} is a sequence
$\langle C_\alpha \mid \alpha \in \kappa^+ \cap {\rm cof}(S) \rangle$
such that
\begin{enumerate}
\item $C_\alpha$ is club in $\alpha$ and ${\rm ot}(C_\alpha) \le \kappa$.
\item If $\beta \in \lim(C_\alpha) \cap \lim(C_{\alpha'})$ then
$C_\alpha \cap \beta = C_{\alpha'} \cap \beta$.
\end{enumerate}
{\em $\square_\kappa^S$ holds} if and only if there is a
{\em $\square_\kappa^S$-sequence}.
\end{definition}
\begin{definition}\label{d1}
For each infinite cardinal $\kappa$, a regular cardinal
$\mu$ is {\em safe for $\kappa$} if and only if
\begin{enumerate}
\item $\mu \le \kappa$.
\item For every cardinal $\lambda \le \kappa$, if $\lambda$ is
$\kappa^+$ supercompact then
$\lambda \le \mu$.
\end{enumerate}
${\rm Safe}(\kappa)$ is the set of safe regular cardinals for $\kappa$.
\end{definition}
We note that the safe set is a final segment of ${\rm REG} \cap (\kappa+1)$, and that
the safe set can only be empty when $\kappa$ is a singular
limit of cardinals which are $\kappa^+$ supercompact.
In addition, by the remarks immediately following
the statement of Theorem \ref{tgf}, ${\rm Safe}(\gg)$
is upwards absolute to any cardinal and cofinality
preserving generic extension by a partial ordering admitting
a closure point at $\go$ and preserving all regular instances of supercompactness.
\section{The Proof of Theorem \ref{t2}}\label{s2}
We turn now to the proof of Theorem \ref{t2}.
\begin{proof}
Suppose
$V \models ``$ZFC + GCH + $\K \neq
\emptyset$ is the class of
supercompact cardinals''.
By Theorem \ref{t1}, we may assume in addition that in $V$,
level by level equivalence holds, and that
$\square^S_\gk$ holds
for every infinite cardinal $\gk$,
where $S = {\rm Safe}(\gk)$.
We are in a position to define the partial ordering $\FP$
used in the proof of Theorem \ref{t2}.
%We fix $\lambda$ a cardinal with $2^\lambda = \lambda^+$.
We pattern our definition after the iteration found in \cite[Section 3.2]{AC08}.
First, for $\gl$ a cardinal,
let $\FQ^\diamondsuit(\lambda^+)$ be the partial ordering of
\cite[page 71]{AC08} which adds $\diamondsuit^+_{\lambda^+}$.
For the exact definition, we refer readers to \cite{AC08}. We note only that
$\FQ^\diamondsuit(\lambda^+)$ is $\lambda^+$-directed closed and $\lambda^{++}$-c.c.
$\FP = \la \la \FP_\gd, \dot \FQ_\gd \ra \mid \gd \in {\rm ORD} \ra$
may now be defined as the proper class Easton support
iteration which begins by forcing with $\add(\go, 1)$ (i.e.,
$\FP_0 = \{\emptyset\}$ and $\FQ_0 = \add(\go, 1)$)
so as to ensure a closure point at $\go$.
We then let $\dot \FQ_\gd$ be a term for
\begin{enumerate}
\item $\add(\gd, 1)$ for $\gd$ inaccessible.
%or $\gd$ the successor of a singular cardinal.
%\item The lottery sum of $\add(\gd, \gd^{+})$ and $\FQ^\diamondsuit(\gd)$
%at cardinals $\gd$ where $\gd = \gl^{++}$ for $\gl$ a singular cardinal.
\item The lottery sum of $\add(\gd, \gd^{+})$ and $\FQ^\diamondsuit(\gd)$
at cardinals $\gd$ where $\gd = \gl^{+}$ for $\gl$ the successor
of a singular cardinal (so in particular, $\gl = \gr^+$ and $\gd = \gr^{++}$ where $\gr$ is
a singular cardinal).
%\item The partial ordering $\FQ^\diamondsuit(\gd)$
%at cardinals $\gd$ where $\gd = \gl^{+}$ for $\gl$ a %non-inaccessible
%regular cardinal which is not the successor of a singular cardinal.
\item The partial ordering $\FQ^\diamondsuit(\gd)$
at cardinals $\gd$ where $\gd = \gl^{+}$ and $\gl$ is a %non-inaccessible
regular cardinal which is not the successor of a singular cardinal
(so in particular, either $\gl$ is inaccessible, or $\gl = \gr^+$ where
$\gr$ is a regular cardinal).
\item Trivial forcing if $\gd$ does not fall into any of the above three categories
(so in particular, trivial forcing occurs if either $\gd$ is a singular cardinal or
$\gd = \gl^+$ and $\gl$ is a singular cardinal). %, as well as elsewhere).
\end{enumerate}
%$\FP$ then
%does nontrivial forcing only at cardinals $\gl^+$ where $\gl$ is singular.
%At such a $\gl$, $\dot \FQ_\gl$ is a term for the lottery sum of
%$\add(\gl^+, \gl^{++})$ and $\FQ^\diamondsuit(\lambda^+)$.
As in \cite{AC08},
we need to show that forcing with $\FP$
preserves all regular instances of supercompactness.
Standard arguments show that $V^\FP \models {\rm ZFC}$ and that
forcing with $\FP$ preserves all cardinals, cofinalities, and GCH.
% and cofinalities, together with GCH and the fact that $V^{\FP}$ is a model of ZFC.
In addition, in analogy to what was done in \cite{AC08},
using the arguments of \cite[Lemma 1.1]{A05}
and \cite[Theorem 12.2]{CFM}, %as was done in \cite{AC08},
it is easily
verified that in $V^{\FP}$, $\diamondsuit_\mu$
holds for every $\mu$ which is
inaccessible, and %or the successor of a singular cardinal, and
$\diamondsuit^+_\mu$ holds
at cardinals $\gm$ where $\gm = \gl^{+}$ for $\gl$ a %non-inaccessible
regular cardinal which is not the successor of a singular cardinal.
%for every $\mu$ which is
% the double successor of a regular cardinal.
Since GCH holds in $V^\FP$, by Shelah's work of \cite{Sh10},
$\diamondsuit_\mu$ holds in $V^\FP$ for every successor cardinal $\mu$
and hence holds in $V^\FP$ for every regular cardinal $\mu$.
\begin{lemma}\label{l1}
If $V \models ``\gk < \gl$ are such that $\gk$ is $\gl$ supercompact
and $\gl$ is regular'', then
$V^\FP \models ``\gk$ is $\gl$ supercompact''.
\end{lemma}
\begin{proof}
Let $\gk < \gl$ be as in the hypotheses of Lemma \ref{l1}.
If $\gl$ is either inaccessible or $\gl = \gd^+$ where
$\gd$ is %the successor of
a singular cardinal, then the argument that
$V^\FP \models ``\gk$ is $\gl$ supercompact''
is exactly the same as in
\cite[Theorem 5, %pages 73--74,
bottom of page 73 up to and including the first
three paragraphs on page 74]{AC08}.
%(when $\gl$ is inaccessible) or
If $\gl = \gd^+$ where $\gd$ is a regular cardinal
which is not the successor of a singular cardinal, then
%the successor of a regular cardinal, then non-inaccessible regular cardinal, then
the argument that
$V^\FP \models ``\gk$ is $\gl$ supercompact''
is exactly the same as in
%\cite[Theorem 5, pages 73--74,
%case where $\gg$ is inaccessible or the
%successor of a singular cardinal]{AC08} (when $\gl$ is inaccessible)
\cite[Theorem 5, fourth paragraph on page 74 through the end of
the proof on page 76]{AC08}.
%(when $\gl = \gd^+$ for $\gd$ the successor of a non-inaccessible regular cardinal).
Suppose now that $\gl = \gd^+$ where $\gd$ is the successor of a singular cardinal.
%i.e., $\gl = \gd^{++}$ where $\gd$ is a singular cardinal.
Assume that $\FQ^\diamondsuit_\gl$ is chosen in the stage $\gl$
lottery held in the definition of $\FP$, and that we are forcing above $p_0 \in \FP$
which forces that this is indeed the case.
The argument that
$V^\FP \models ``\gk$ is $\gl$ supercompact''
is then once again exactly the same as in
\cite[Theorem 5, fourth paragraph on page 74 through the end of
the proof on page 76]{AC08}.
If $\add(\gl, \gl^+)$ is chosen in the stage $\gl$
lottery held in the definition of $\FP$, then
the argument that
$V^\FP \models ``\gk$ is $\gl$ supercompact''
%is the one found on \cite[pages 591--592]{A03} suitably modified.
combines standard techniques with
ideas originally due to Magidor \cite{Ma2}.
Variants of Magidor's method are also given in
\cite[pages 119--120]{AS97a} as well as \cite[Lemma 2.4]{A01} and are found
other places in the literature as well.
However, since the proof requires certain modifications
%since the relevant constructions require certain modifications
from its original version, we present it completely below.
Getting specific, suppose $j : V \to M$ is an elementary embedding
witnessing the $\gl$ supercompactness of $\gk$ which is generated
by a supercompact ultrafilter over $P_\gk(\gl)$.
%Let $\gl = \gd^+$, where $\gd$ is the successor of a singular cardinal.
%Let $\gl = \gd^{++}$, where $\gd$ is a singular cardinal.
Assume we are forcing above $p_1 \in \FP$ which forces
$\add(\gl, \gl^+)$ to be chosen in the stage $\gl$ lottery held
in the definition of $\FP$.
This allows us (with a slight abuse of notation) to write
$\FP = \FP_\gk \ast \dot \FP(\gk, \gl) \ast \dot \add(\gl, \gl^+)
\ast \dot \FQ$, where %\ast \dot \add(j(\gl), j(\gl^+))$, where
$\dot \FP(\gk, \gl)$ is a term for the portion of $\FP$ acting on
ordinals in the half-open interval $[\gk, \gl)$ and $\dot \FQ$ is a
term for the portion of $\FP$ acting on ordinals above $\gl$.
Let $G_0$ be $V$-generic over $\FP_\gk$, $G_1$ be
$V[G_0]$-generic over $\FP(\gk, \gl)$, and $G_3$ be
$V[G_0][G_1]$-generic over $\add(\gl, \gl^+)$.
Write $j(\FP_\gk \ast \dot \FP(\gk, \gl) \ast \dot \add(\gl, \gl^+)) =
\FP_\gk \ast \dot \FP(\gk, \gl) \ast \dot \add(\gl, \gl^+)) \ast \dot \FR
\ast \dot \FP(j(\gk), j(\gl)) \ast \dot \add(j(\gl), j(\gl^+))$, where
$\dot \FR$ is a term for the portion of $j(\FP)$ acting on ordinals
in the open interval $(\gl, j(\gk))$.
We construct
in $V[G_0][G_1][G_2]$ an $M[G_0][G_1][G_2]$-generic object $G_3$ over $\FR$,
an $M[G_0][G_1][G_2][G_3]$-generic object $G_4$ over $\FP(j(\gk), j(\gl))$,
and an $M[G_0][G_1][G_2][G_3][G_4]$-generic object $G_5$ over
$(\add(j(\gl), j(\gl^+))^{M[G_0][G_1][G_2][G_3][G_4]}$
such that $j''(G_0 \ast G_1 \ast G_2) \subseteq G_0 \ast G_1 \ast G_2 \ast G_3 \ast G_4 \ast G_5$.
This allows us to lift $j : V \to M$ in $V[G_0][G_1][G_2]$ to the elementary embedding
$j : V[G_0][G_1][G_2] \to M[G_0][G_1][G_2][G_3][G_4][G_5]$ witnessing the $\gl$ supercompactness
of $\gk$ in $V[G_0][G_1][G_2]$. Since
$\forces_{\FP_\gk \ast \dot \FP(\gk, \gl) \ast \dot \add(\gl, \gl^+)} ``\dot \FQ$ is
$\gl^+$-directed closed'', this will suffice to show that
$V^\FP \models ``\gk$ is $\gl$ supercompact''.
%For the convenience of readers, we present these arguments below.
%We begin by observing that since $\card{\FP_\gk \ast \dot \FP(\gk, \gl)} \le \gd^+ < \gl$,
%$M[G_0][G_1]$ remains $\gl$-closed with respect to $V[G_0][G_1]$.
We begin by observing that since $\FP_\gk \ast \dot \FP(\gk, \gl) \ast \dot
\add(\gl, \gl^+)$ is $\gl^+$-c.c.,
$M[G_0][G_1][G_2]$ remains $\gl$-closed with respect to $V[G_0][G_1][G_2]$.
In $V$, since $M$
is given via an ultrapower by a
normal measure over $P_\gk(\gl)$,
$\card{j(\gk)}$ and $\card{j(\gk^+)}$ may be calculated as
$\card{\{f \mid f : P_\gk(\gl) \to \gk\}} =
\card{\{f \mid f : \gl \to \gk\}} =
2^\gl = \gl^+$ and
$\card{\{f \mid f : P_\gk(\gl) \to \gk^+\}} =
\card{\{f \mid f : \gl \to \gk^+\}} = %\card{[\gl^+]^\gl}
2^\gl = \gl^+$ respectively.
Also, by elementarity, since $V \models ``2^\gk = \gk^+$'',
$M \models ``2^{j(\gk)} = (j(\gk))^+ = j(\gk^+)$''.
%Because $(\add(\gk, \gk^+))^{V[G_0]}$ is $\gk^+$-c.c$.$ in $V[G_0]$,
%\gl$M[G_0][G_1][G_2]$ remains $\gl$-closed with respect to $V[G_0][G_1]$.
In addition, since $M[G_0][G_1][G_2] \models ``\FR$ is an Easton support
iteration of length $j(\gk)$'', $M[G_0][G_1][G_2] \models ``\card{\FR} = j(\gk)$ and
$2^{j(\gk)} = (j(\gk))^+ = j(\gk^+)$''. %$\FR$ is $j(\gl)$-c.c.''.
This means the number of dense open subsets of $\FR$
present in $M[G_0][G_1][G_2]$ is $j(\gk^+)$. Further, as
$M[G_0][G_1][G_2] \models ``\FR$ is $\gl^+$-directed closed'' and
$M[G_0][G_1][G_2]$ is $\gl$-closed with respect to $V[G_0][G_1][G_2]$,
$\FR$ is $\gl^+$-directed closed in $V[G_0][G_1][G_2]$ as well.
Since $\gl^+$ is preserved from $V$ to
$V[G_0][G_1][G_2]$, we may let
$\la D_\gb \mid \gb < \gl^+ \ra \in V[G_0][G_1][G_2]$
enumerate the dense open subsets of $\FR$ present in $M[G_0][G_1][G_2]$.
We may now use the fact that $\FR$ is
$\gl^+$-directed closed in $V[G_0][G_1][G_2]$ to meet each $D_\gb$
and thereby construct in $V[G_0][G_1][G_2]$
an $M[G_0][G_1][G_2]$-generic
object $G_3$ over $\FR$. Our construction guarantees that
$j '' G_0 \subseteq G_0 \ast G_1 \ast G_2 \ast G_3$,
so $j$ lifts in $V[G_0][G_1][G_2]$ to
$j : V[G_0] \to M[G_0][G_1][G_2][G_3]$.
By the fact that $\FR$ is $\gl^+$-directed closed in %both
$M[G_0][G_1][G_2]$, %and $V[G_0][G_1]$,
$M[G_0][G_1][G_2][G_3]$ remains $\gl$-closed with respect to
$V[G_0][G_1][G_2][G_3] = V[G_0][G_1][G_2]$.
Therefore, since $V[G_0] \models ``\card{\FP(\gk, \gl)} < \gl$'',
$M[G_0][G_1][G_2][G_3] \models ``\card{\FP(j(\gk), j(\gl))} < j(\gl)$''
and $j '' G_1 \in M[G_0][G_1][G_2][G_3]$.
Also, by its definition,
$M[G_0][G_1][G_2][G_3] \models ``\FP(j(\gk), j(\gl))$ is $j(\gk)$-directed closed'',
so since $j(\gk) > \gl^+$,
$M[G_0][G_1][G_2][G_3] \models ``\FP(j(\gk), j(\gl))$ is $\gl^+$-directed closed'' as well.
Since it is once again the case that
$V[G_0][G_1][G_2] \models ``\FP(j(\gk), j(\gl))$ is $\gl^+$-directed closed'',
this means we can let $q^*$ be a master condition for $j '' G_1$ and use the
construction mentioned in the previous paragraph %earlier in this paragraph
to build in
$V[G_0][G_1][G_2]$ an $M[G_0][G_1][G_2][G_3]$-generic object $G_4$ for
$\FP(j(\gk), j(\gl))$ such that $q^* \in G_4$.
Our construction guarantees that $j '' (G_0 \ast G_1) \subseteq
G_0 \ast G_1 \ast G_2 \ast G_3 \ast G_4$, so we may lift $j$ to
$j : V[G_0][G_1] \to M[G_0][G_1][G_2][G_3][G_4]$.
Once again, because
$M[G_0][G_1][G_2][G_3] \models ``\FP(j(\gk), j(\gl))$ is $\gl^+$-directed closed'',
$M[G_0][G_1][G_2][G_3][G_4]$ remains $\gl$-closed with respect to
$V[G_0][G_1][G_2][G_3][G_4] = \break V[G_0][G_1][G_2]$.
We now use Magidor's methods mentioned above to
construct in $V[G_0][G_1][G_2]$ an \break
$M[G_0][G_1][G_2][G_3][G_4]$-generic object $G_5$ over
$(\add(j(\gl), j(\gl^+))^{M[G_0][G_1][G_2][G_3][G_4]}$
such that \break
$j''(G_0 \ast G_1 \ast G_2) \subseteq G_0 \ast G_1 \ast G_2 \ast G_3 \ast G_4 \ast G_5$.
We follow the presentation given in the proof of \cite[Lemma 2.4]{A01}.
For $\gz \in (\gl, \gl^{+})$ and
$p \in (\add(\gl, \gl^{+}))^{V[G_0][G_1]}$, let %\break
$p \rest \gz = \{\la \la \rho, \gs \ra, \eta \ra \in p \mid
\gs < \gz\}$ and
$G_2 \rest \gz = \{p \rest \gz \mid p \in G_2\}$. Clearly,
$V[G_0][G_1][G_2] \models %\break
``|G_2 \rest \gz| \le \gl$
for all $\gz \in (\gl, \gl^{+})$''. Thus, since
${\add(j(\gl), j(\gl^{+}))}^{M[G_0][G_1][G_2][G_3][G_4]}$ is
$j(\gl)$-directed closed and $j(\gl) > \gl^{+}$,
$q_\gz = \bigcup\{j(p) \mid p \in G_2 \rest \gz\}$ is
well-defined and is an element of %\break
$(\add(j(\gl), j(\gl^{+})))^{M[G_0][G_1][G_2][G_3][G_4]}$.
Further, if
$\la \rho, \gs \ra \in \dom(q_\gz) -
\dom(\bigcup_{\gb < \gz} q_\gb)$
($\bigcup_{\gb < \gz} q_\gb$ is well-defined by closure),
then
$\gs \in [\bigcup_{\gb < \gz} j(\gb), j(\gz))$. To see this,
assume to the contrary that
$\gs < \bigcup_{\gb < \gz} j(\gb)$. Let
$\gb$ be minimal such that $\gs < j(\gb)$.
It must thus be the case that for some
$p \in G_2 \rest \gz$,
$\la \rho, \gs \ra \in \dom(j(p))$.
Since by elementarity and the definitions of
$G_2 \rest \gb$ and $G_2 \rest \gz$, for
$p \rest \gb = q \in G_2 \rest \gb$,
$j(q) = j(p) \rest j(\gb) = j(p \rest \gb)$,
it must be the case that
$\la \rho, \gs \ra \in \dom(j(q))$. This means
$\la \rho, \gs \ra \in \dom(q_\gb)$, a contradiction.
Since GCH is preserved to $M[G_0][G_1][G_2][G_3][G_4]$,
%\models ``j(\gl)$ is inaccessible and $2^{j(\gl)} = j(\gl^+)$'',
an application of \cite[Lemma 15.4, page 227]{J} shows that
%\break
$M[G_0][G_1][G_2][G_3][G_4] \models ``\add(j(\gl),
j(\gl^{+}))$ is
$j(\gl^+)$-c.c$.$ and has
$j(\gl^{+})$ many maximal antichains''.
This means that if
${\cal A} \in M[G_0][G_1][G_2][G_3][G_4]$ is a
maximal antichain of $\add(j(\gl), j(\gl^{+}))$,
${\cal A} \subseteq \add(j(\gl), \gb)$ for some
$\gb \in (j(\gl), j(\gl^{+}))$. Thus, since
%the fact $V \models ``2^\gl = \gl^+$''
%and the fact $j$ is generated by a normal measure over
%$\gl$ imply that
$V \models ``|j(\gl^{+})| =
\card{\{f \mid f : P_\gk(\gl) \to \gl^+\}} =
\card{\{f \mid f : \gl \to \gl^+\}} =
\card{[\gl^+]^\gl} = \gl^{+}$'', we can let
$\la {\cal A}_\gz \mid \gz \in (\gl, \gl^{+}) \ra \in
V[G_0][G_1][G_2]$ be an enumeration of all of the
maximal antichains of $\add(j(\gl), j(\gl^{+}))$
present in
$M[G_0][G_1][G_2][G_3][G_4]$.
%Working in $V[G_0][G_1][G_2]$, we define
We define now an increasing sequence
$\la r_\gz \mid \gz \in (\gl, \gl^{+}) \ra$ of
elements of $\add(j(\gl), j(\gl^{+}))$ such that
$\forall \gz \in (\gl, \gl^{+}) [r_\gz \ge q_\gz$ and
$r_\gz \in \add(j(\gl), j(\gz))]$ and such that
$\forall {\cal A} \in
\la {\cal A}_\gz \mid \gz \in (\gl, \gl^{+}) \ra
\exists \gb \in (\gl, \gl^{+})
\exists r \in {\cal A} [r_\gb \ge r]$.
Assuming we have such a sequence,
$G_5 = \{p \in \add(j(\gl), j(\gl^{+})) \mid \break
\exists r \in \la r_\gz \mid \gz \in (\gl, \gl^{+}) \ra
[r \ge p]\}$ is an
$M[G_0][G_1][G_2][G_3][G_4]$-generic object over \break
$(\add(j(\gl), j(\gl^{+})))^{M[G_0][G_1][G_2][G_3][G_4]}$. To define
$\la r_\gz \mid \gz \in (\gl, \gl^{+}) \ra$, if
$\gz$ is a limit, we let
$r_\gz = \bigcup_{\gb \in (\gl, \gz)} r_\gb$.
By the facts
$\la r_\gb \mid \gb \in (\gl, \gz) \ra$
is (strictly) increasing and
$M[G_0][G_1][G_2][G_3][G_4]$ is
$\gl$-closed with respect to
$V[G_0][G_1][G_2]$, this definition is valid.
Assuming now $r_\gz$ has been defined and
we wish to define $r_{\gz + 1}$, let
$\la {\cal B}_\gb \mid \gb < \eta \le \gl \ra$
be the subsequence of
$\la {\cal A}_\gb \mid \gb \le \gz + 1 \ra$
containing each antichain ${\cal A}$ such that
${\cal A} \subseteq \add(j(\gl), j(\gz + 1))$.
Because
$q_\gz, r_\gz \in \add(j(\gl), j(\gz))$,
$q_{\gz + 1} \in \add(j(\gl), j(\gz + 1))$, and
$j(\gz) < j(\gz + 1)$, the condition
$r_{\gz + 1}' = r_\gz \cup q_{\gz + 1}$ is
well-defined. This is since by our earlier observations,
any new elements of
$\dom(q_{\gz + 1})$ won't be present in either
$\dom(q_\gz)$ or $\dom(r_\gz)$.
We can thus, using the fact
$M[G_0][G_1][G_2][G_3][G_4]$ is $\gl$-closed
%under $\gl^+$ sequences
with respect to
$V[G_0][G_1][G_2]$, define by induction
an increasing sequence
$\la s_\gb \mid \gb < \eta \ra$ such that
$s_0 \ge r_{\gz + 1}'$,
$s_\rho = \bigcup_{\gb < \rho} s_\gb$ if
$\rho$ is a limit ordinal, and
$s_{\gb + 1} \ge s_\gb$ is such that
$s_{\gb + 1}$ extends some element of
${\cal B}_\gb$. The just mentioned
closure fact implies
$r_{\gz + 1} = \bigcup_{\gb < \eta} s_\gb$
is a well-defined condition.
In order to show that $G_5$ is
$M[G_0][G_1][G_2][G_3][G_4]$-generic over
$\add(j(\gl), j(\gl^{+}))$, we must show that
$\forall {\cal A} \in
\la {\cal A}_\gz \mid \gz \in (\gl, \gl^{+}) \ra
\exists \gb \in (\gl, \gl^{+})
\exists r \in {\cal A} [r_\gb \ge r]$.
To do this, we first note that
$\la j(\gz) \mid \gz < \gl^{+} \ra$ is
unbounded in $j(\gl^{+})$. To see this, if
$\gb < j(\gl^{+})$ is an ordinal, then for some
$f : P_\gk(\gl) \to M$ representing $\gb$,
we can assume that for $p \in P_\gk(\gl)$,
$f(p) < \gl^{+}$. Thus, by the regularity of
$\gl^{+}$ in $V$ and the fact that
$V \models ``\card{P_\gk(\gl)} = \gl$'',
$\gb_0 = \bigcup_{\gr < \gl} f(\gr) <
\gl^{+}$, and $j(\gb_0) > \gb$.
This means by our earlier remarks that if
${\cal A} \in \la {\cal A}_\gz \mid \gz <
\gl^{+} \ra$, ${\cal A} = {\cal A}_\rho$,
then we can let
$\gb \in (\gl, \gl^{+})$ be such that
${\cal A} \subseteq \add(j(\gl), j(\gb))$.
By construction, for $\eta > \max(\gb, \rho)$,
there is some $r \in {\cal A}$ such that
$r_\eta \ge r$.
And, as any
$p \in \add(\gl, \gl^{+})$ is such that for some
$\gz \in (\gl, \gl^{+})$, $p = p \rest \gz$,
$G_5$ is such that if
$p \in G_2$, $j(p) \in G_5$.
This means that
$j''(G_0 \ast G_1 \ast G_2) \subseteq G_0 \ast G_1 \ast G_2 \ast G_3 \ast G_4 \ast G_5$,
thereby completing the proof of Lemma \ref{l1}.
%This completes the proof of Lemma \ref{l1}.
%(when $\gl = \gd^+$ for $\gd$ the successor of a non-inaccessible regular cardinal).
\end{proof}
Lemma \ref{l1} immediately implies that all $V$-supercompact
cardinals are preserved to $V^\FP$.
By its definition, we may write
$\FP = \FP' \ast \dot \FP''$, where $\card{\FP'} = \go$,
$\FP' = \add(\go, 1)$ is nontrivial, and
$\forces_{\FP'} ``\dot \FP''$ is $\ha_1$-directed closed''.
Therefore, by our remarks in the paragraph immediately following
Theorem \ref{tgf}, $\K$ remains the class of supercompact
cardinals in $V^\FP$.
Further, by the upwards absoluteness of any form of square in a
cardinal preserving generic extension (see the discussion given in
the proof of \cite[Theorem 1]{A05}) and our remarks in the last
paragraph of Section \ref{s1},
in $V^\FP$, $\square^S_\gg$ holds for every infinite cardinal $\gg$,
where $S = {\rm Safe}(\gg)$.
\begin{lemma}\label{l2}
$V^\FP \models ``$Level by level equivalence
%between strong compactness and supercompactness
holds''.
\end{lemma}
\begin{proof}
We mimic the proofs of \cite[Lemma 1.3]{A05} and
\cite[Lemma 4.1]{AC08}. Suppose
$V^\FP \models ``\gk < \gl$ are regular cardinals such that
$\gk$ is $\gl$ strongly compact and $\gk$ isn't a
measurable limit of cardinals $\gd$ which are $\gl$ supercompact''.
By Lemma \ref{l1}, any cardinal $\gd$ such that
$\gd$ is $\gl$ supercompact in $V$ remains
$\gl$ supercompact in $V^\FP$. We may therefore infer that
$V \models ``\gk < \gl$ are regular cardinals such that
$\gk$ isn't a measurable limit of cardinals $\gd$
which are $\gl$ supercompact''.
By the definition of $\FP$, it is easily seen that
$\FP$ is mild with respect to $\gk$. Hence, by
the factorization of $\FP$ given above and
Theorem \ref{tgf}, $V \models ``\gk$ is
$\gl$ strongly compact''. Consequently, by level by level
equivalence between strong compactness and supercompactness
in $V$, $V \models ``\gk$ is $\gl$ supercompact'', so
another application of Lemma \ref{l1} yields that
$V^\FP \models ``\gk$ is $\gl$ supercompact''.
This completes the proof of Lemma \ref{l2}.
\end{proof}
\begin{lemma}\label{l3}
$V^\FP \models ``V = {\rm HOD}$''.
\end{lemma}
\begin{proof}
We use ideas given by Brooke-Taylor in \cite[Theorem 9]{BT09} (see also the proof of
\cite[Lemma 4.3]{AF11}).
In particular, to show that $V^\FP \models ``V = {\rm HOD}$'', it will suffice
to show that every set of ordinals in $V^\FP$ is ordinal definable using a coding
oracle given by %failures of
where $\diamondsuit^*_{\gk^{++}}$ holds or fails for $\gk$ a singular cardinal.
To do this, suppose $p \in \FP$, $\dot x$, and $\ga$ are such that
$p \forces ``\dot x \subseteq \ga$'' and that $\ga$ is a limit ordinal.
By the definition of $\FP$, there must exist some ordinal $\gb$ such that
$p \forces ``\dot x \in V^{\FP_\gb}$''.
Also, since $\FP$ is an Easton support proper class length iteration, there must be some
ordinal $\gg$ such that ${\rm support}(p) \subseteq \gg$.
This allows us to write $p = \la p_\gs \mid \gs < \gg \ra$.
Let $\gd > \max(\ga, \gb, \gg)$ be fixed but arbitrary, with
$\la \gd_\gs \mid \gs < \ga \ra$ the first $\ga$ many singular cardinals
greater than $\gd$.
Define $\gr = \sup(\{\gd_\gs \mid \gs < \ga\})$.
Take $q > p$, $q = \la q_\gs \mid \gs < \gr \ra$ as the condition
such that $q_\gs = p_\gs$ for $\gs < \gg$.
For $\gs \ge \gg$, $\gs < \gr$, $q_\gs$ is the trivial condition, except
if $\gz < \ga$ and $\gs = \gd^{++}_\gz$.
At such a $\gs$, $q_\gs$ is defined as the term such that
$\forces_{\FP_\gs} ``q_\gs \in \dot \FQ_\gs$ forces that
$\dot \FQ^\diamondsuit(\gs)$ is chosen in the stage $\gs$ lottery if $\gz \in \dot x$, but
$\dot \add(\gs, \gs^+)$ is chosen in the stage $\gs$ lottery if $\gz \not\in \dot x$''.
%The arguments found in the paragraph immediately preceding Lemma \ref{l1}
The definition of $\FP$
tells us that in $V^\FP$, $\diamondsuit^+_\gs$, and hence also $\diamondsuit^*_\gs$,
both hold if $\FQ^\diamondsuit(\gs)$ is chosen in the stage $\gs$ lottery.
On the other hand, the arguments found in \cite[paragraph immediately
preceding Section 3, pages 644--645]{BT09} combined with the closure properties of $\FP$
tell us that $\diamondsuit^*_\gs$ fails if
$\add(\gs, \gs^+)$ is chosen in the stage $\gs$ lottery.
This means that as in the proofs of \cite[Theorem 9]{BT09} and \cite[Lemma 4.3]{AF11},
the proper class of conditions forcing that the set $x$ is coded using the
coding oracle mentioned in the first paragraph of the proof of this lemma is
dense in $\FP$.
Since $x$ is an arbitrary set of ordinals, again
as in the proofs of \cite[Theorem 9]{BT09} and \cite[Lemma 4.3]{AF11},
$V^\FP \models ``V = {\rm HOD}$''.
This completes the proof of Lemma \ref{l3}.
\end{proof}
Lemmas \ref{l1} -- \ref{l3}, the paragraph immediately
preceding the proof of Lemma \ref{l1},
and the intervening remarks complete the proof of Theorem \ref{t2}.
\end{proof}
\begin{pf}
Turning now to the proof of Theorem \ref{t2a}, suppose
$V \models ``$ZFC + GCH + $\K \neq
\emptyset$ is the class of
supercompact cardinals''.
Assume in addition that in $V$, there is a proper class of measurable cardinals.
By \cite[Theorem 1]{A07}, we may further assume that $V$ satisfies
level by level equivalence and that every measurable cardinal $\gk$ in $V$
carries $2^{2^\gk} = \gk^{++}$ many normal measures (which is of course
the maximal number of normal measures a $V$-measurable cardinal can carry).
We pattern the definition of the partial ordering used in the
proof of Theorem \ref{t2a} after the definition of the forcing conditions
$\FP^0$ used in the proof of \cite[Theorem 2]{A07}. Specifically,
let $\la \gd_\ga \mid \ga \in {\rm Ord} \ra$ enumerate all $V$-measurable
cardinals which are not themselves limits of $V$-measurable cardinals.
By our assumption that $V$ contains a proper class of measurable cardinals,
such an enumeration is possible.
The partial ordering $\FP = \la \la \FP_\gd, \dot \FQ_\gd \ra \mid \gd \in {\rm Ord} \ra$
may now be defined as the proper class Easton support iteration which begins
by forcing with $\add(\go, 1)$
so as once again to ensure a closure point at $\go$.
$\dot \FQ_\gd$ is then a term for trivial forcing, except if $\gd$ is such that $\gd = \gs^+$ where
$\gs$ is a $V$-measurable cardinal which is not a limit of $V$-measurable cardinals.
In this case, $\dot \FQ_\gd$ is a term for the lottery sum of trivial forcing and
${\rm Coll}(\gd^+, \gd^{++})$.
As in the proof of Theorem \ref{t2},
standard arguments show $V^\FP \models {\rm ZFC}$ and that
forcing with $\FP$ preserves GCH.
In addition, the arguments in the proof of \cite[Theorem 4.2, pages 369--371]{AF11}
show that $V^\FP \models ``\K$ is the class of supercompact cardinals +
There is a proper class of measurable cardinals + $V = {\rm HOD}$ + GA''.
Thus, the proof of Theorem \ref{t2a} is completed by the following lemma.
\begin{lemma}\label{l4}
$V^\FP \models ``$Level by level equivalence holds''.
\end{lemma}
\begin{proof}
To prove Lemma \ref{l4}, we will show that if
$\gk < \gl$ are such that
$V^\FP \models ``\gk$ is $\gl$ strongly compact and $\gl$ is regular'', then
$V^\FP \models ``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
of cardinals $\gd$ which are $\gl$ supercompact''.
Towards this end, suppose $\gk < \gl$ are as just stated.
%such that $V^\FP \models ``\gk$ is $\gl$ strongly compact and $\gl$ is regular''.
Write $\FP = \FP' \ast \dot \FP''$, where
$\card{\FP'} = \go$, $\FP' = \add(\go, 1)$ is nontrivial, and
$\forces_{\FP'} ``\dot \FP''$ is $\ha_1$-directed closed''.
This factorization, combined with $\FP$'s definition, yield that
%By its definition,
$\FP$ admits a closure point at $\go$ and is mild with respect to $\gk$.
Therefore, by Theorem \ref{tgf}, $V \models ``\gk$ is $\gl$ strongly compact''.
We consider now two cases.
\bigskip\noindent Case 1: $\gl$ is a trivial stage of forcing, i.e.,
either $\gl = \gs^+$, where $\gs$ is in $V$ a measurable cardinal
which is not a limit of measurable cardinals and trivial forcing is chosen
in the stage $\gs^+$ lottery held in the definition of $\FP$, or
$\gl \neq \gs^+$, where $\gs$ is in $V$ a measurable cardinal
which is not a limit of measurable cardinals.
Because level by level equivalence holds in $V$, we may consequently infer that
$V \models ``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
of cardinals $\gd$ which are $\gl$ supercompact''.
We will prove that
$V^\FP \models
``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
of cardinals $\gd$ which are $\gl$ supercompact''.
This means we can now
let $\gd \le \gk$ be such that $V \models ``\gd$ is $\gl$ supercompact''.
We will show that $V^\FP \models ``\gd$ is $\gl$ supercompact''.
%This is enough to prove Lemma \ref{l4}, since
It will then follow that
$V^\FP \models ``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
of cardinals $\gd$ which are $\gl$ supercompact''.
Towards this end,
write $\FP = \FP_\gd \ast \dot \FP(\gd, \gl) \ast \dot \FP^\gl$, where
$\dot \FP(\gd, \gl)$ is a term for the portion of $\FP$ such that
$\FP_\gd \ast \dot \FP(\gd, \gl) = \FP_{\gl + 1}$
%which is defined using ordinals in the closed interval $[\gd, \gl]$
and $\dot \FP^\gl$ is a term for the rest of $\FP$. It is then the case that
$\forces_{\FP_\gd \ast \dot \FP(\gd, \gl)} ``\dot \FP^\gl$ is
$\gl^+$-directed closed''.
%$\gl'$-directed closed for $\gl'$ the least inaccessible cardinal greater than $\gl$''.
Thus, to prove that $V^\FP \models ``\gd$ is $\gl$ supercompact'',
%``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
%of cardinals $\gg$ which are $\gl$ supercompact'',
it will suffice to show that
$V^{\FP_\gd \ast \dot \FP(\gd, \gl)} \models ``\gd$ is $\gl$ supercompact''.
%``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
%of cardinals $\gg$ which are $\gl$ supercompact''.
To do this,
%suppose $\gd \le \gk$ is such that
%$V \models ``\gd$ is $\gl$ supercompact''.
%\bigskip\noindent Case 1: $\gl = \gg^{++}$ where $\gg$ is in $V$ a measurable cardinal
%which is not a limit of measurable cardinals and
%${\rm Coll}(\gg^+, \gg^{++})$ is chosen
%in the stage $\gl$ lottery held in the definition of $\FP$.
let $G$ be $V$-generic over $\FP_\gd \ast \dot \FP(\gd, \gl)$, with
%$G = G_\gk \ast G(\gk, \gl)$
$G = G_0 \ast G_1$ the corresponding factorization of $G$.
%Write $\FP_\gd \ast \dot \FP(\gd, \gl) = \FQ^* \ast \dot \FQ^{**}$, where
%$\card{\FQ^*} = \go$, $\FQ^* = \add(\go, 1)$ is nontrivial, and
%$\forces_{\FQ^*} ``\dot \FQ^{**}$ is $\ha_2$-directed closed''.
%Suppose $\gd \le \gk$ is such that $V \models ``\gd$ is $\gl$ supercompact''.
%We note it cannot be true that
%We note it cannot be the case that for any $\gd \le \gk$ such that
%$V \models ``\gd$ is $\gl$ supercompact'', it is also true that
%$V \models ``\gl = \gg^+$, $\gg$ is a measurable cardinal which
%is not a limit of measurable cardinals, and supercompactness
%first fails at $\gg^{++} = \gl^+$'' if
%${\rm Coll}(\gg^+, \gg^{++})$ is chosen
%in the stage $\gl$ lottery held in the definition of $\FP$.
%For, if this were the case, then
%$V^{\FP_\gd \ast \dot \FP(\gd, \gl)} \models ``\card{(\gl^{+})^V} = \gl$
%and $\gd$ is $\gl$ supercompact''.
%Because $\FP_\gd \ast \dot \FP(\gd, \gl)$ admits a gap at $\ha_1$,
%as we observed in the paragraph following its statement, Theorem \ref{tgf} implies that
%$V \models ``\gd$ is $\gl^+$ supercompact'', a contradiction.
%Note that the only possible stages of nontrivial forcing occur at ordinals $\gs^+$
%of the form $\gs = \gg^{++}$,
%where $\gs$ is in $V$ a measurable cardinal
%which is not a limit of measurable cardinals and
%${\rm Coll}(\gs^+, \gs^{++})$ is chosen
%in the stage $\gs^+$ lottery held in the definition of $\FP$.
%If $\gl \neq \gs^+$ for such a $\gs$, then
With a slight abuse of notation,
by assuming we are forcing above the appropriate condition
%abusing notation somewhat,
and using the fact that GCH is preserved to $V^{\FP_\ga}$ for any ordinal $\ga$,
the definition of $\FP$ immediately
allows us to infer that $V[G_0] \models ``\card{\FP(\gd, \gl)} \le \gl$''.
%Define now $\gr = \gl$ if $\gl \neq \gs^+$ for $\gs$ a $V$-measurable cardinal
%which is not a limit of $V$-measurable cardinals, but $\gr = \gl^+$ if $\gl = \gs^+$
%for $\gs$ a $V$-measurable cardinal which is not a limit of $V$-measurable cardinals.
Let $j : V \to M$ be an elementary embedding witnessing the $\gl$
supercompactness of $\gd$ which is generated by a supercompact
ultrafilter over $P_\gd(\gl)$.
Write $j(\FP_\gd \ast \dot \FP(\gd, \gl)) = \FP_\gd \ast \dot \FP(\gd, \gl)
\ast \dot \FR \ast j(\dot \FP(\gd, \gl)) = \FP_\gd \ast \dot \FP(\gd, \gl)
\ast \dot \FR \ast \dot \FP(j(\gd), j(\gl))$.
This means we may use the arguments given in the proof of Lemma \ref{l1} in
the construction of the generic objects $G_3$ and $G_4$ to build in
$V[G_0][G_1]$ an $M[G_0][G_1]$-generic object $G_2$ for $\FR$ and an
$M[G_0][G_1][G_2]$-generic object $G^*_3$ for $\FP(j(\gd), j(\gl))$ and lift in $V[G_0][G_1]$
the embedding $j$ to $j : V[G_0][G_1] \to M[G_0][G_1][G_2][G^*_3]$.
The lifted $j$ is then a witness to the $\gl$ supercompactness of
$\gd$ in $V[G_0][G_1]$.
%Since the lifted $j$ is a witness to the $\gr$ supercompactness of $\gd$
%(and hence the $\gl$ supercompactness of $\gd$) in
%$V[G_0][G_1]$, this completes the proof of Lemma \ref{l4}.
\bigskip\noindent Case 2: $\gl$ is a nontrivial stage of forcing, i.e.,
$\gl = \gs^+$, where $\gs$ is in $V$ a measurable cardinal
which is not a limit of measurable cardinals and
${\rm Coll}(\gs^+, \gs^{++})$ is chosen
in the stage $\gs^+$ lottery held in the definition of $\FP$.
Then because
$V^\FP \models ``\card{(\gs^{++})^V} = \gs^+ = (\gs^+)^V$ and
$\gk$ is $\gl =\gs^+$ strongly compact'',
we know that
$V^\FP \models ``\gk$ is $(\gs^{++})^V$ strongly compact'' as well.
Thus, by the remarks in the paragraph immediately following
Theorem \ref{tgf}, $V \models ``\gk$ is $\gs^{++} = \gl^+$ strongly compact''.
%Hence, without loss of generality, we may replace $\gl$ with $\gl^+$.
Hence, by level by level equivalence,
$V \models ``$Either $\gk$ is $\gl^+$ supercompact, or $\gk$ is a
measurable limit of cardinals $\gd$ which are $\gl^+$ supercompact''.
As in Case 1, let $\gd \le \gk$ be such that $V \models ``\gd$ is $\gl^+$ supercompact''.
We adopt also the same notation as in Case 1.
%Since GCH implies that %under these circumstances
%$\card{{\rm Coll}(\gl, \gl^+)} = \gl^+
%= \card{{\rm Coll}(\gs^+, \gs^{++})} = \gs^{++}$,
%this means by the definition of $\FP$ that we may infer
In analogy to Case 1, once again by slightly abusing notation,
assuming that we are forcing above the appropriate condition,
and using the facts that GCH is preserved to $V^{\FP_\ga}$ for any ordinal $\ga$
and $(\gl^+)^V = (\gl^+)^{V[G_0]}$,
it consequently follows by the definition of $\FP$ that %as in Case 1,
$V[G_0] \models ``\card{\FP(\gd, \gl^+)} = \gl^+$''. %under the current situation as well.
%Let $\eta = (\gl^+)^V$.
We may then repeat the argument of Case 1 to infer that
$V[G_0][G_1] \models ``\gd$ is $(\gl^+)^V$ supercompact''.
As $V[G_0][G_1] \models ``\card{(\gl^+)^V} = \gs^+ = \gl$'' and
$\forces_{\FP_\gd \ast \dot \FP(\gd, \gl^+)} ``\dot \FP^\gl$ is
$\gl'$-directed closed for $\gl'$ the least inaccessible cardinal above $\gl$'',
%, which as before implies that
$V^\FP \models ``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a
measurable limit of cardinals $\gd$ which are $\gl$ supercompact''.
%for $\gr = \gl$ or $\gr = \gl^+$.
\bigskip
Cases 1 and 2 show that regardless if $\gl$ is a trivial stage of forcing,
if $V^\FP \models ``\gk$ is $\gl$ strongly compact'', then
$V^\FP \models ``$Either $\gk$ is $\gl$ supercompact, or
$\gk$ is a measurable limit of cardinals $\gd$ which are $\gl$ supercompact''.
Since this means that $V^\FP \models ``$Level by level equivalence holds'',
the proof of Lemma \ref{l4} is now complete.
\end{proof}
Lemma \ref{l4} and
the paragraph immediately preceding Lemma \ref{l4}
complete the proof of Theorem \ref{t2a}.
\end{pf}
We conclude this paper by asking what other combinatorial properties
can consistently hold in a model containing supercompact cardinals which
satisfies both level by level equivalence and $V = {\rm HOD}$. In particular, can
such a model satisfy the same combinatorial properties as the model
of Theorem \ref{t1}?
Can a model be constructed which satisfies both the combinatorial
properties of Theorem \ref{t2} (or suitable generalizations thereof) and GA?
Can the assumption of a proper class of measurable cardinals be removed
from the proof of Theorem \ref{t2a}?
If these sorts of models were to be constructed via forcing, one would most likely
have to employ different kinds of coding oracles from the ones used above.
\begin{thebibliography}{99}
\bibitem{A05} A.~Apter, ``Diamond, Square, and Level by Level Equivalence'',
{\it Archive for Mathematical Logic 44}, 2005, 387--395.
\bibitem{A01} A.~Apter, ``Expanding $\gk$'s Power Set in its Ultrapowers'',
{\it Radovi Matematicki 10}, 2001, 149--156.
%\bibitem{A03} A.~Apter, ``Failures of GCH and the Level by Level
%Equivalence between Strong Compactness and Supercompactness'',
%{\it Mathematical Logic Quarterly 49}, 2003, 587--597.
\bibitem{A07} A.~Apter, ``Level by Level Equivalence and the Number
of Normal Measures over $P_\gk(\gl)$'', {\it Fundamenta Mathematicae 194},
2007, 253--265.
\bibitem{AC08} A.~Apter, J.~Cummings, ``An $L$-like Model
Containing Very Large Cardinals'', {\it Archive for Mathematical Logic 47},
2008, 65--78.
\bibitem{AF11} A.~Apter, Sh$.$ Friedman,
``Coding into HOD via Normal Measures with Some Applications'',
{\it Mathematical Logic Quarterly 57}, 2011, 366--372.
\bibitem{AS97a} A.~Apter, S.~Shelah, ``On the Strong
Equality between Supercompactness and Strong Compactness'',
{\it Transactions of the American Mathematical Society 349},
1997, 103--128.
%\bibitem{AS97b} A.~Apter, S.~Shelah, ``Menas' Result is
%Best Possible'',
%{\it Transactions of the American Mathematical Society 349},
%1997, 2007--2034.
\bibitem{BT09} A.~Brooke-Taylor, ``Large Cardinals and Definable
Well-Orders on the Universe'', {\it Journal of Symbolic Logic 74}, 2009, 641--654.
\bibitem{CFM} J.~Cummings, M.~Foreman,
M.~Magidor, ``Squares, Scales, and
Stationary Reflection'', {\it Journal of
Mathematical Logic 1}, 2001, 35--98.
\bibitem{VWS} M.~Foreman, M.~Magidor,
``A Very Weak Square Principle'',
{\it Journal of Symbolic Logic 62}, 1997, 175--196.
%\bibitem{F00} S.~D.~Friedman, {\it Fine Structure and Class Forcing},
%de Gruyter Series in Logic and Its Applications, volume 3,
%de Gruyter, Berlin, 2000.
\bibitem{F06} S.~D.~Friedman, ``Large Cardinals and
$L$-like Universes'', in: {\it Set Theory: Recent Trends and
Applications}, Alessandro Andretta, editor, {\bf Quaderni di
Matematica}, volume 17, 2005, 93--110.
\bibitem{FHR} G.~Fuchs, J.~D.~Hamkins, J.~Reitz,
``Set-Theoretic Geology'', {\it Annals of Pure and Applied Logic 166}, 2015, 464--501.
\bibitem{H03} J.~D.~Hamkins, ``Extensions with the
Approximation and Cover Properties have No New
Large Cardinals'', {\it Fundamenta Mathematicae 180}, 2003, 257--277.
\bibitem{H2} J.~D.~Hamkins, ``Gap Forcing'',
{\it Israel Journal of Mathematics 125}, 2001, 237--252.
\bibitem{H3} J.~D.~Hamkins, ``Gap Forcing:
Generalizing the L\'evy-Solovay Theorem'',
{\it Bulletin of Symbolic Logic 5}, 1999, 264--272.
%\bibitem{H} J.~D.~Hamkins, {\it Lifting and
%Extending Measures; Fragile Measurability},
%Doctoral Dissertation, University of California,
%Berkeley, 1994.
\bibitem{H4} J.~D.~Hamkins, ``The Lottery Preparation'',
{\it Annals of Pure and Applied Logic 101},
2000, 103--146.
%\bibitem{H5} J.~D.~Hamkins, ``Small Forcing Makes
%Any Cardinal Superdestructible'',
%{\it Journal of Symbolic Logic 63}, 1998, 51--58.
\bibitem{J} T.~Jech, {\it Set Theory:
The Third Millennium Edition,
Revised and Expanded}, Springer-Verlag,
Berlin and New York, 2003.
\bibitem{KM} Y.~Kimchi, M.~Magidor, ``The Independence
between the Concepts of Compactness and Supercompactness'',
circulated manuscript.
%\bibitem{L07} R.~Laver, ``Certain Very Large Cardinals are not
%Created in Small Forcing Extensions'', {\it Annals of Pure and Applied Logic 149},
%2007, 1--6.
%\bibitem{L} R.~Laver, ``Making the Supercompactness of $\gk$ Indestructible
%under $\gk$-Directed Closed Forcing'', {\it Israel Journal of Mathematics 29},
%1978, 385--388.
%\bibitem{LS} A.~L\'evy, R.~Solovay,
%``Measurable Cardinals and the Continuum Hypothesis'',
%{\it Israel Journal of Mathematics 5}, 1967, 234--248.
%\bibitem{Ma} M.~Magidor, ``How Large is the First
%Strongly Compact Cardinal? or A Study on
%Identity Crises'', {\it Annals of
%Mathematical Logic 10}, 1976, 33--57.
\bibitem{Ma2} M.~Magidor, ``On the Existence of Nonregular
Ultrafilters and the Cardinality of Ultrapowers'', {\it Transactions of the
American Mathematical Society 249}, 1979, 97--111.
\bibitem{Me} T.~Menas, ``On Strong Compactness and
Supercompactness'', {\it Annals of Mathematical Logic 7},
1974, 327--359.
\bibitem{R07} J.~Reitz, ``The Ground Axiom'', {\it Journal of
Symbolic Logic 72}, 2007, 1299--1317.
\bibitem{Sh10} S.~Shelah, ``Diamonds'', {\it Proceedings of the
American Mathematical Society 138}, 2010, 2151--2161.
%\bibitem{So} R.~Solovay, ``Strongly Compact Cardinals
%and the GCH'', in: {\it Proceedings of the Tarski
%Symposium}, {\bf Proceedings of Symposia in Pure
%Mathematics 25}, American Mathematical Society,
%Providence, 1974, 365--372.
%\bibitem{SRK} R.~Solovay, W.~Reinhardt, A.~Kanamori,
%``Strong Axioms of Infinity and Elementary Embeddings'',
%{\it Annals of Mathematical Logic 13}, 1978, 73--116.
\bibitem{Wo17} W.~H.~Woodin, ``In Search of Ultimate-$L$: The 19th
Midrasha Mathematicae Lectures'', {\it Bulletin of Symbolic Logic 23}, 2017, 1--109.
\end{thebibliography}
\end{document}
We now use arguments originally due to
Magidor \cite{Ma2}, which are also given in
\cite[pages 119--120]{AS97a} and are found
other places in the literature as well, to construct
in $V[G_0][G_1]$ an $M[G_0][H_1][H_2]$-generic
object $H_3$ over $(\add(j(\gk), j(\gk^+))^{M[G_0][H_1][H_2]}$
such that $j''(G_0 \ast G_1) \subseteq G_0 \ast H_1 \ast H_2 \ast H_3$.
For the convenience of readers, we present these
arguments below.
For $\gz \in (\gk, \gk^{+})$ and
$p \in \add(\gk, \gk^{+})$, let
$p \rest \gz = \{\la \la \rho, \gs \ra, \eta \ra \in p \mid
\gs < \gz\}$ and
$G_1 \rest \gz = \{p \rest \gz \mid p \in G_1\}$. Clearly,
$V[G_0][G_1] \models ``|G_1 \rest \gz| \le \gk$
for all $\gz \in (\gk, \gk^{+})$''. Thus, since
${\add(j(\gk), j(\gk^{+}))}^{M[G_0][H_1][H_2]}$ is
$j(\gk)$-directed closed and $j(\gk) > \gk^{+}$,
$q_\gz = \bigcup\{j(p) \mid p \in G_1 \rest \gz\}$ is
well-defined and is an element of
${\add(j(\gk), j(\gk^{+}))}^{M[G_0][H_1][H_2]}$.
Further, if
$\la \rho, \gs \ra \in \dom(q_\gz) -
\dom(\bigcup_{\gb < \gz} q_\gb)$
($\bigcup_{\gb < \gz} q_\gb$ is well-defined by closure),
then
$\gs \in [\bigcup_{\gb < \gz} j(\gb), j(\gz))$. To see this,
assume to the contrary that
$\gs < \bigcup_{\gb < \gz} j(\gb)$. Let
$\gb$ be minimal such that $\gs < j(\gb)$.
It must thus be the case that for some
$p \in G_1 \rest \gz$,
$\la \rho, \gs \ra \in \dom(j(p))$.
Since by elementarity and the definitions of
$G_1 \rest \gb$ and $G_1 \rest \gz$, for
$p \rest \gb = q \in G_1 \rest \gb$,
$j(q) = j(p) \rest j(\gb) = j(p \rest \gb)$,
it must be the case that
$\la \rho, \gs \ra \in \dom(j(q))$. This means
$\la \rho, \gs \ra \in \dom(q_\gb)$, a contradiction.
Since $M[G_0][H_1][H_2] \models ``j(\gk)$ is inaccessible and
$2^{j(\gk)} = j(\gk^+)$'', an application of \cite[Lemma 15.4, page 227]{J} shows that
%\break
$M[G_0][H_1][H_2] \models ``\add(j(\gk),
j(\gk^{+}))$ is
$j(\gk^+)$-c.c$.$ and has
$j(\gk^{+})$ many maximal antichains''.
This means that if
${\cal A} \in M[G_0][H_1][H_2]$ is a
maximal antichain of \break $\add(j(\gk), j(\gk^{+}))$,
${\cal A} \subseteq \add(j(\gk), \gb)$ for some
$\gb \in (j(\gk), j(\gk^{+}))$. Thus, since
%the fact $V \models ``2^\gk = \gk^+$''
%and the fact $j$ is generated by a normal measure over
%$\gk$ imply that
$V \models ``|j(\gk^{+})| = \gk^{+}$'', we can let
$\la {\cal A}_\gz \mid \gz \in (\gk, \gk^{+}) \ra \in
V[G_0][G_1]$ be an enumeration of all of the
maximal antichains of $\add(j(\gk), j(\gk^{+}))$
present in
$M[G_0][H_1][H_2]$.
Working in $V[G_0][G_1]$, we define
now an increasing sequence
$\la r_\gz \mid \gz \in (\gk, \gk^{+}) \ra$ of
elements of $\add(j(\gk), j(\gk^{+}))$ such that
$\forall \gz \in (\gk, \gk^{+}) [r_\gz \ge q_\gz$ and
$r_\gz \in \add(j(\gk), j(\gz))]$ and such that
$\forall {\cal A} \in
\la {\cal A}_\gz \mid \gz \in (\gk, \gk^{+}) \ra
\exists \gb \in (\gk, \gk^{+})
\exists r \in {\cal A} [r_\gb \ge r]$.
Assuming we have such a sequence,
$H_3 = \{p \in \add(j(\gk), j(\gk^{+})) \mid
\exists r \in \la r_\gz \mid \gz \in (\gk, \gk^{+}) \ra
[r \ge p]\}$ is an
$M[G_0][H_1][H_2]$-generic object over
$\add(j(\gk), j(\gk^{+}))$. To define
$\la r_\gz \mid \gz \in (\gk, \gk^{+}) \ra$, if
$\gz$ is a limit, we let
$r_\gz = \bigcup_{\gb \in (\gk, \gz)} r_\gb$.
By the facts
$\la r_\gb \mid \gb \in (\gk, \gz) \ra$
is (strictly) increasing and
$M[G_0][H_1][H_2]$ is
$\gk$-closed with respect to
$V[G_0][G_1]$, this definition is valid.
Assuming now $r_\gz$ has been defined and
we wish to define $r_{\gz + 1}$, let
$\la {\cal B}_\gb \mid \gb < \eta \le \gk \ra$
be the subsequence of
$\la {\cal A}_\gb \mid \gb \le \gz + 1 \ra$
containing each antichain ${\cal A}$ such that
${\cal A} \subseteq \add(j(\gk), j(\gz + 1))$.
Because
$q_\gz, r_\gz \in \add(j(\gk), j(\gz))$,
$q_{\gz + 1} \in \add(j(\gk), j(\gz + 1))$, and
$j(\gz) < j(\gz + 1)$, the condition
$r_{\gz + 1}' = r_\gz \cup q_{\gz + 1}$ is
well-defined. This is since by our earlier observations,
any new elements of
$\dom(q_{\gz + 1})$ won't be present in either
$\dom(q_\gz)$ or $\dom(r_\gz)$.
We can thus, using the fact
$M[G_0][H_1][H_2]$ is $\gk$-closed
%under $\gk^+$ sequences
with respect to
$V[G_0][G_1]$, define by induction
an increasing sequence
$\la s_\gb \mid \gb < \eta \ra$ such that
$s_0 \ge r_{\gz + 1}'$,
$s_\rho = \bigcup_{\gb < \rho} s_\gb$ if
$\rho$ is a limit ordinal, and
$s_{\gb + 1} \ge s_\gb$ is such that
$s_{\gb + 1}$ extends some element of
${\cal B}_\gb$. The just mentioned
closure fact implies
$r_{\gz + 1} = \bigcup_{\gb < \eta} s_\gb$
is a well-defined condition.
In order to show that $H_3$ is
$M[G_0][H_1][H_2]$-generic over
$\add(j(\gk), j(\gk^{+}))$, we must show that
$\forall {\cal A} \in
\la {\cal A}_\gz \mid \gz \in (\gk, \gk^{+}) \ra
\exists \gb \in (\gk, \gk^{+})
\exists r \in {\cal A} [r_\gb \ge r]$.
To do this, we first note that
$\la j(\gz) \mid \gz < \gk^{+} \ra$ is
unbounded in $j(\gk^{+})$. To see this, if
$\gb < j(\gk^{+})$ is an ordinal, then for some
$f : \gk \to M$ representing $\gb$,
we can assume that for $\gr < \gk$,
$f(\gr) < \gk^{+}$. Thus, by the regularity of
$\gk^{+}$ in $V$,
$\gb_0 = \bigcup_{\gr < \gk} f(\gr) <
\gk^{+}$, and $j(\gb_0) > \gb$.
This means by our earlier remarks that if
${\cal A} \in \la {\cal A}_\gz \mid \gz <
\gk^{+} \ra$, ${\cal A} = {\cal A}_\rho$,
then we can let
$\gb \in (\gk, \gk^{+})$ be such that
${\cal A} \subseteq \add(j(\gk), j(\gb))$.
By construction, for $\eta > \max(\gb, \rho)$,
there is some $r \in {\cal A}$ such that
$r_\eta \ge r$.
And, as any
$p \in \add(\gk, \gk^{+})$ is such that for some
$\gz \in (\gk, \gk^{+})$, $p = p \rest \gz$,
$H_3$ is such that if
$p \in G_1$, $j(p) \in H_3$.
\end{proof}
\begin{lemma}\label{l1}
If $V \models ``\gk < \gl$ are such that $\gk$ is $\gl$ supercompact
and $\gl$ is regular'', then
$V^\FP \models ``\gk$ is $\gl$ supercompact''.
\end{lemma}
\begin{proof}
Let $\gk < \gl$ be as in the hypotheses of Lemma \ref{l1}.
If $\gl$ is either inaccessible or $\gl = \gd^+$ where
$\gd$ is the successor of a non-inaccessible regular cardinal, then
the argument that
$V^\FP \models ``\gk$ is $\gl$ supercompact''
is exactly the same as in
%\cite[Theorem 5, pages 73--74,
%case where $\gg$ is inaccessible or the
%successor of a singular cardinal]{AC08} (when $\gl$ is inaccessible)
\cite[Theorem 5, %pages 73--74,
bottom of page 73 up to and including the first
three paragraphs on page 74]{AC08} (when $\gl$ is inaccessible) or
\cite[Theorem 5, fourth paragraph on page 74 through the end of
the proof on page 76]{AC08} (when $\gl = \gd^+$ for $\gd$
the successor of a non-inaccessible regular cardinal).
Suppose now that $\gl$ is the successor of a singular cardinal.
\end{proof}
We now use Magidor's methods mentioned above to
construct in $V[G_0][G_1][G_2]$
an \break $M[G_0][G_1][G_2][G_3]$-generic object $G_4$ over
$(\add(j(\gl), j(\gl^+))^{M[G_0][G_1][G_2][G_3]}$
such that \break
$j''(G_0 \ast G_1 \ast G_2) \subseteq G_0 \ast G_1 \ast G_2 \ast G_3 \ast G_4$.
For $\gz \in (\gl, \gl^{+})$ and
$p \in (\add(\gl, \gl^{+}))^{V[G_0][G_1]}$, let \break
$p \rest \gz = \{\la \la \rho, \gs \ra, \eta \ra \in p \mid
\gs < \gz\}$ and
$G_2 \rest \gz = \{p \rest \gz \mid p \in G_2\}$. Clearly,
$V[G_0][G_1][G_2] \models \break ``|G_2 \rest \gz| \le \gl$
for all $\gz \in (\gl, \gl^{+})$''. Thus, since
${\add(j(\gl), j(\gl^{+}))}^{M[G_0][G_1][G_2][G_3]}$ is
$j(\gl)$-directed closed and $j(\gl) > \gl^{+}$,
$q_\gz = \bigcup\{j(p) \mid p \in G_2 \rest \gz\}$ is
well-defined and is an element of \break
$(\add(j(\gl), j(\gl^{+})))^{M[G_0][G_1][G_2][G_3]}$.
Further, if
$\la \rho, \gs \ra \in \dom(q_\gz) -
\dom(\bigcup_{\gb < \gz} q_\gb)$
($\bigcup_{\gb < \gz} q_\gb$ is well-defined by closure),
then
$\gs \in [\bigcup_{\gb < \gz} j(\gb), j(\gz))$. To see this,
assume to the contrary that
$\gs < \bigcup_{\gb < \gz} j(\gb)$. Let
$\gb$ be minimal such that $\gs < j(\gb)$.
It must thus be the case that for some
$p \in G_2 \rest \gz$,
$\la \rho, \gs \ra \in \dom(j(p))$.
Since by elementarity and the definitions of
$G_2 \rest \gb$ and $G_2 \rest \gz$, for
$p \rest \gb = q \in G_2 \rest \gb$,
$j(q) = j(p) \rest j(\gb) = j(p \rest \gb)$,
it must be the case that
$\la \rho, \gs \ra \in \dom(j(q))$. This means
$\la \rho, \gs \ra \in \dom(q_\gb)$, a contradiction.
\begin{lemma}\label{l5}
$V^\FP \models ``$Level by level equivalence holds''.
%If $V \models ``\gk < \gl$ are such that $\gk$ is $\gl$ supercompact
%and $\gl$ is regular'', then
%$V^\FP \models ``\gk$ is $\gl$ supercompact''.
\end{lemma}
\begin{proof}
To prove Lemma \ref{l5}, we will show that if
$\gk < \gl$ are such that
$V^\FP \models ``\gk$ is $\gl$ strongly compact and $\gl$ is regular'', then
$V^\FP \models ``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
of cardinals $\gg$ which are $\gl$ supercompact''.
Towards this end, suppose $\gk < \gl$ are as just stated.
%such that $V^\FP \models ``\gk$ is $\gl$ strongly compact and $\gl$ is regular''.
Write $\FP = \FP^* \ast \dot \FP^{**}$, where
$\card{\FP^*} = \go$, $\FP^* = \add(\go, 1)$ is nontrivial, and
$\forces_{\FP^*} ``\dot \FP^{**}$ is $\ha_2$-directed closed''.
This factorization, combined with $\FP$'s definition, yield that
%By its definition,
$\FP$ admits a gap at $\ha_1$ and is mild with respect to $\gk$.
Therefore, by Theorem \ref{tgf}, $V \models ``\gk$ is $\gl$ strongly compact''.
Because level by level equivalence holds in $V$, we may consequently infer that
$V \models ``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
of cardinals $\gg$ which are $\gl$ supercompact''.
If we now write $\FP = \FP_\gk \ast \dot \FP(\gk, \gl) \ast \dot \FP^\gl$ where
$\dot \FP(\gk, \gl)$ is a term for the portion of $\FP$ which is defined using
ordinals in the closed interval $[\gk, \gl]$
and $\dot \FP^\gl$ is a term for the rest of $\FP$, then it is the case that
$\forces_{\FP_\gk \ast \dot \FP(\gk, \gl)} ``\dot \FP^\gl$ is $\gl'$-directed closed for
$\gl'$ the least inaccessible cardinal greater than $\gl$''.
Thus, to show that $V^\FP \models ``$Either $\gk$ is $\gl$ supercompact,
or $\gk$ is a measurable limit of cardinals $\gg$ which are $\gl$ supercompact'',
it will suffice to show that
$V^{\FP_\gk \ast \dot \FP(\gk, \gl)} \models ``$Either $\gk$ is $\gl$ supercompact,
or $\gk$ is a measurable limit of cardinals $\gg$ which are $\gl$ supercompact''.
To do this, let $G$ be $V$-generic over $\FP_\gk \ast \dot \FP(\gk, \gl)$, with
%$G = G_\gk \ast G(\gk, \gl)$
$G = G_0 \ast G_1$ the corresponding factorization of $G$.
Write $\FP_\gk \ast \dot \FP(\gk, \gl) = \FQ^* \ast \dot \FQ^{**}$, where
$\card{\FQ^*} = \go$, $\FQ^* = \add(\go, 1)$ is nontrivial, and
$\forces_{\FQ^*} ``\dot \FQ^{**}$ is $\ha_2$-directed closed''.
Suppose $\gd \le \gk$ is such that $V \models ``\gd$ is $\gl$ supercompact''.
We note it cannot be true that
%We note it cannot be the case that for any $\gd \le \gk$ such that
%$V \models ``\gd$ is $\gl$ supercompact'', it is also true that
$V \models ``\gl = \gg^+$, $\gg$ is a measurable cardinal which
is not a limit of measurable cardinals, and supercompactness
first fails at $\gg^{++} = \gl^+$'' if ${\rm Coll}(\gg^+, \gg^{++})$ is chosen
in the stage $\gl$ lottery held in the definition of $\FP$.
For, if this were the case, then
$V^{\FP_\gd \ast \dot \FP(\gd, \gl)} \models ``\card{(\gl^{+})^V} = \gl$
and $\gd$ is $\gl$ supercompact''.
Because $\FP_\gd \ast \dot \FP(\gd, \gl)$ admits a gap at $\ha_1$,
as we observed in the paragraph following its statement, Theorem \ref{tgf} implies that
$V \models ``\gd$ is $\gl^+$ supercompact'', a contradiction.
Since the only possible stages of nontrivial forcing occur
if $\gl = \gg^+$ is such a cardinal,
and since GCH implies that under these circumstances $\card{{\rm Coll}(\gl, \gl^+)} = \gl^+
= \card{{\rm Coll}(\gg^+, \gg^{++})} = \gg^{++}$,
%this means by the definition of $\FP$ that we may infer
it consequently follows by the definition of $\FP$ that $\card{\FP(\gd, \gl)} < \gl$.
Let now $j : V \to M$ be an elementary embedding witnessing the $\gl$
supercompactness of $\gd$ which is generated by a supercompact
ultrafilter over $P_\gd(\gl)$.
Write $j(\FP_\gd \ast \dot \FP(\gd, \gl)) =$
This means we may use the arguments given in the proof of Lemma \ref{l1} to
\end{proof}
\begin{lemma}\label{l5}
$V^\FP \models ``$Level by level equivalence holds''.
%If $V \models ``\gk < \gl$ are such that $\gk$ is $\gl$ supercompact
%and $\gl$ is regular'', then
%$V^\FP \models ``\gk$ is $\gl$ supercompact''.
\end{lemma}
\begin{proof}
To prove Lemma \ref{l5}, we will show that if
$\gk < \gl$ are such that
$V^\FP \models ``\gk$ is $\gl$ strongly compact and $\gl$ is regular'', then
$V^\FP \models ``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
of cardinals $\gg$ which are $\gl$ supercompact''.
Towards this end, suppose $\gk < \gl$ are as just stated.
%such that $V^\FP \models ``\gk$ is $\gl$ strongly compact and $\gl$ is regular''.
Write $\FP = \FP^* \ast \dot \FP^{**}$, where
$\card{\FP^*} = \go$, $\FP^* = \add(\go, 1)$ is nontrivial, and
$\forces_{\FP^*} ``\dot \FP^{**}$ is $\ha_2$-directed closed''.
This factorization, combined with $\FP$'s definition, yield that
%By its definition,
$\FP$ admits a gap at $\ha_1$ and is mild with respect to $\gk$.
Therefore, by Theorem \ref{tgf}, $V \models ``\gk$ is $\gl$ strongly compact''.
Because level by level equivalence holds in $V$, we may consequently infer that
$V \models ``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
of cardinals $\gg$ which are $\gl$ supercompact''.
This means we can now
let $\gd \le \gk$ be such that $V \models ``\gd$ is $\gl$ supercompact''.
We will show that $V^\FP \models ``\gd$ is $\gl$ supercompact''.
This is enough to prove Lemma \ref{l5}, since it will then follow that
$V^\FP \models ``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
of cardinals $\gd$ which are $\gl$ supercompact''.
Towards this end,
write $\FP = \FP_\gd \ast \dot \FP(\gd, \gl) \ast \dot \FP^\gl$, where
$\dot \FP(\gd, \gl)$ is a term for the portion of $\FP$ which is defined using
ordinals in the closed interval $[\gd, \gl]$
and $\dot \FP^\gl$ is a term for the rest of $\FP$. It is then the case that
$\forces_{\FP_\gd \ast \dot \FP(\gd, \gl)} ``\dot \FP^\gl$ is $\gl'$-directed closed for
$\gl'$ the least inaccessible cardinal greater than $\gl$''.
Thus, to show that $V^\FP \models ``\gd$ is $\gl$ supercompact'',
it will suffice to show that
$V^{\FP_\gd \ast \dot \FP(\gd, \gl)} \models ``\gd$ is $\gl$ supercompact''.
To do this, let $G$ be $V$-generic over $\FP_\gd \ast \dot \FP(\gd, \gl)$, with
%$G = G_\gk \ast G(\gk, \gl)$
$G = G_0 \ast G_1$ the corresponding factorization of $G$.
Write $\FP_\gd \ast \dot \FP(\gd, \gl) = \FQ^* \ast \dot \FQ^{**}$, where
$\card{\FQ^*} = \go$, $\FQ^* = \add(\go, 1)$ is nontrivial, and
$\forces_{\FQ^*} ``\dot \FQ^{**}$ is $\ha_2$-directed closed''.
%Suppose $\gd \le \gk$ is such that $V \models ``\gd$ is $\gl$ supercompact''.
We note it cannot be true that
%We note it cannot be the case that for any $\gd \le \gk$ such that
%$V \models ``\gd$ is $\gl$ supercompact'', it is also true that
$V \models ``\gl = \gg^+$, $\gg$ is a measurable cardinal which
is not a limit of measurable cardinals, and supercompactness
first fails at $\gg^{++} = \gl^+$'' if ${\rm Coll}(\gg^+, \gg^{++})$ is chosen
in the stage $\gl$ lottery held in the definition of $\FP$.
For, if this were the case, then
$V^{\FP_\gd \ast \dot \FP(\gd, \gl)} \models ``\card{(\gl^{+})^V} = \gl$
and $\gd$ is $\gl$ supercompact''.
Because $\FP_\gd \ast \dot \FP(\gd, \gl)$ admits a gap at $\ha_1$,
as we observed in the paragraph following its statement, Theorem \ref{tgf} implies that
$V \models ``\gd$ is $\gl^+$ supercompact'', a contradiction.
Since the only possible stages of nontrivial forcing occur
if $\gl = \gg^+$ is such a cardinal,
and since GCH implies that under these circumstances $\card{{\rm Coll}(\gl, \gl^+)} = \gl^+
= \card{{\rm Coll}(\gg^+, \gg^{++})} = \gg^{++}$,
%this means by the definition of $\FP$ that we may infer
it consequently follows by the definition of $\FP$ that $\card{\FP(\gd, \gl)} \le \gl$.
Let now $j : V \to M$ be an elementary embedding witnessing the $\gl$
supercompactness of $\gd$ which is generated by a supercompact
ultrafilter over $P_\gd(\gl)$.
Write $j(\FP_\gd \ast \dot \FP(\gd, \gl)) = \FP_\gd \ast \dot \FP(\gd, \gl)
\ast \dot \FR \ast j(\dot \FP(\gd, \gl)) = \FP_\gd \ast \dot \FP(\gd, \gl)
\ast \dot \FR \ast \dot \FP(j(\gd), j(\gl))$.
This means we may use the arguments given in the proof of Lemma \ref{l1} in
the construction of the generic objects $G_3$ and $G_4$ to build in
$V[G_0][G_1]$ an $M[G_0][G_1]$-generic object $G_2$ for $\FR$ and an
$M[G_0][G_1][G_2]$-generic object $G_3$ for $\FP(j(\gd), j(\gl))$ and lift in $V[G_0][G_1]$
the embedding $j$ to $j : V[G_0][G_1] \to M[G_0][G_1][G_2][G_3]$.
Since the lifted $j$ is a witness to the $\gl$ supercompactness of $\gd$ in
$V[G_0][G_1]$, this completes the proof of Lemma \ref{l5}.
\end{proof}
\begin{lemma}\label{l4}
$V^\FP \models ``$Level by level equivalence holds''.
%If $V \models ``\gk < \gl$ are such that $\gk$ is $\gl$ supercompact
%and $\gl$ is regular'', then
%$V^\FP \models ``\gk$ is $\gl$ supercompact''.
\end{lemma}
\begin{proof}
To prove Lemma \ref{l4}, we will show that if
$\gk < \gl$ are such that
$V^\FP \models ``\gk$ is $\gl$ strongly compact and $\gl$ is regular'', then
$V^\FP \models ``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
of cardinals $\gg$ which are $\gl$ supercompact''.
Towards this end, suppose $\gk < \gl$ are as just stated.
%such that $V^\FP \models ``\gk$ is $\gl$ strongly compact and $\gl$ is regular''.
Write $\FP = \FP^* \ast \dot \FP^{**}$, where
$\card{\FP^*} = \go$, $\FP^* = \add(\go, 1)$ is nontrivial, and
$\forces_{\FP^*} ``\dot \FP^{**}$ is $\ha_2$-directed closed''.
This factorization, combined with $\FP$'s definition, yield that
%By its definition,
$\FP$ admits a gap at $\ha_1$ and is mild with respect to $\gk$.
Therefore, by Theorem \ref{tgf}, $V \models ``\gk$ is $\gl$ strongly compact''.
Because level by level equivalence holds in $V$, we may consequently infer that
$V \models ``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
of cardinals $\gg$ which are $\gl$ supercompact''.
We will show that
$V^\FP \models
``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
of cardinals $\gg$ which are $\gl$ supercompact''.
This means we can now
let $\gd \le \gk$ be such that $V \models ``\gd$ is $\gl$ supercompact''.
We will show that $V^\FP \models ``\gd$ is $\gl$ supercompact''.
This is enough to prove Lemma \ref{l4}, since it will then follow that
$V^\FP \models ``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
of cardinals $\gd$ which are $\gl$ supercompact''.
Towards this end,
write $\FP = \FP_\gd \ast \dot \FP(\gd, \gl) \ast \dot \FP^\gl$, where
$\dot \FP(\gd, \gl)$ is a term for the portion of $\FP$ such that
$\FP_\gd \ast \dot \FP(\gd, \gl) = \FP_{\gl + 1}$
%which is defined using ordinals in the closed interval $[\gd, \gl]$
and $\dot \FP^\gl$ is a term for the rest of $\FP$. It is then the case that
$\forces_{\FP_\gd \ast \dot \FP(\gk, \gl)} ``\dot \FP^\gl$ is $\gl'$-directed closed for
$\gl'$ the least inaccessible cardinal greater than $\gl$''.
Thus, to show that $V^\FP \models ``\gd$ is $\gl$ supercompact'',
%``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
%of cardinals $\gg$ which are $\gl$ supercompact'',
it will suffice to show that
$V^{\FP_\gd \ast \dot \FP(\gd, \gl)} \models ``\gd$ is $\gl$ supercompact''.
%``$Either $\gk$ is $\gl$ supercompact, or $\gk$ is a measurable limit
%of cardinals $\gg$ which are $\gl$ supercompact''.
To do this,
%suppose $\gd \le \gk$ is such that
%$V \models ``\gd$ is $\gl$ supercompact''.
%\bigskip\noindent Case 1: $\gl = \gg^{++}$ where $\gg$ is in $V$ a measurable cardinal
%which is not a limit of measurable cardinals and
%${\rm Coll}(\gg^+, \gg^{++})$ is chosen
%in the stage $\gl$ lottery held in the definition of $\FP$.
let $G$ be $V$-generic over $\FP_\gd \ast \dot \FP(\gd, \gl)$, with
%$G = G_\gk \ast G(\gk, \gl)$
$G = G_0 \ast G_1$ the corresponding factorization of $G$.
%Write $\FP_\gd \ast \dot \FP(\gd, \gl) = \FQ^* \ast \dot \FQ^{**}$, where
%$\card{\FQ^*} = \go$, $\FQ^* = \add(\go, 1)$ is nontrivial, and
%$\forces_{\FQ^*} ``\dot \FQ^{**}$ is $\ha_2$-directed closed''.
%Suppose $\gd \le \gk$ is such that $V \models ``\gd$ is $\gl$ supercompact''.
%We note it cannot be true that
%We note it cannot be the case that for any $\gd \le \gk$ such that
%$V \models ``\gd$ is $\gl$ supercompact'', it is also true that
%$V \models ``\gl = \gg^+$, $\gg$ is a measurable cardinal which
%is not a limit of measurable cardinals, and supercompactness
%first fails at $\gg^{++} = \gl^+$'' if
%${\rm Coll}(\gg^+, \gg^{++})$ is chosen
%in the stage $\gl$ lottery held in the definition of $\FP$.
%For, if this were the case, then
%$V^{\FP_\gd \ast \dot \FP(\gd, \gl)} \models ``\card{(\gl^{+})^V} = \gl$
%and $\gd$ is $\gl$ supercompact''.
%Because $\FP_\gd \ast \dot \FP(\gd, \gl)$ admits a gap at $\ha_1$,
%as we observed in the paragraph following its statement, Theorem \ref{tgf} implies that
%$V \models ``\gd$ is $\gl^+$ supercompact'', a contradiction.
Note that the only possible stages of nontrivial forcing occur at ordinals $\gs^+$
%of the form $\gs = \gg^{++}$,
where $\gs$ is in $V$ a measurable cardinal
which is not a limit of measurable cardinals and
${\rm Coll}(\gs^+, \gs^{++})$ is chosen
in the stage $\gs$ lottery held in the definition of $\FP$.
If $\gl \neq \gs^+$ for such a $\gs$, then the definition of $\FP$ immediately
allows us to infer that $\card{\FP(\gd, \gl)} \le \gl$.
If, however, $\gl = \gs^+$ is such a cardinal, then because
$V^\FP \models ``\card{(\gs^{++})^V} = \gs^+ = (\gs^+)^V$ and
$\gd$ is $\gl =\gs^+$ supercompact'',
we know that
$V^\FP \models ``\gd$ is $(\gs^{++})^V$ supercompact'' as well.
Thus, by Theorem \ref{tgf}, $V \models ``\gd$ is $\gs^{++} = \gl^+$ supercompact''.
%Hence, without loss of generality, we may replace $\gl$ with $\gl^+$.
Since GCH implies that under these circumstances $\card{{\rm Coll}(\gl, \gl^+)} = \gl^+
= \card{{\rm Coll}(\gs^+, \gs^{++})} = \gs^{++}$,
%this means by the definition of $\FP$ that we may infer
it consequently follows by the definition of $\FP$ that $\card{\FP(\gd, \gl)} \le \gl$
under the current situation as well.
Define now $\gr = \gl$ if $\gl \neq \gs^+$ for $\gs$ a $V$-measurable cardinal
which is not a limit of $V$-measurable cardinals, but $\gr = \gl^+$ if $\gl = \gs^+$
for $\gs$ a $V$-measurable cardinal which is not a limit of $V$-measurable cardinals.
Let $j : V \to M$ be an elementary embedding witnessing the $\gr$
supercompactness of $\gd$ which is generated by a supercompact
ultrafilter over $P_\gd(\gr)$.
Write $j(\FP_\gd \ast \dot \FP(\gd, \gr)) = \FP_\gd \ast \dot \FP(\gd, \gr)
\ast \dot \FR \ast j(\dot \FP(\gd, \gr)) = \FP_\gd \ast \dot \FP(\gd, \gr)
\ast \dot \FR \ast \dot \FP(j(\gd), j(\gr))$.
This means we may use the arguments given in the proof of Lemma \ref{l1} in
the construction of the generic objects $G_3$ and $G_4$ to build in
$V[G_0][G_1]$ an $M[G_0][G_1]$-generic object $G_2$ for $\FR$ and an
$M[G_0][G_1][G_2]$-generic object $G_3$ for $\FP(j(\gr), j(\gl))$ and lift in $V[G_0][G_1]$
the embedding $j$ to $j : V[G_0][G_1] \to M[G_0][G_1][G_2][G_3]$.
Since the lifted $j$ is a witness to the $\gr$ supercompactness of $\gd$
(and hence the $\gl$ supercompactness of $\gd$) in
$V[G_0][G_1]$, this completes the proof of Lemma \ref{l4}.
\end{proof}
\begin{lemma}\label{l5}
Suppose $V \models ``\gk$ is a measurable cardinal which is not a
limit of measurable cardinals''.
If trivial forcing is selected in the
stage $\gk^+$ lottery held in the definition of $\FP$, then
$V^\FP \models ``\gk$ is a measurable cardinal
which carries $2^{2^\gk} = \gk^{++}$ many normal measures''.
If ${\rm Coll}(\gk^+, \gk^{++})$ is selected in the
stage $\gk^+$ lottery held in the definition of $\FP$, then
$V^\FP \models ``\gk$ is a measurable cardinal
which carries $\gk^+$ many normal measures''.
\end{lemma}
\begin{proof}
Write $\FP = \FP_{\gk^+ + 1} \ast \dot \FQ$.
Since $\forces_{\FP_{\gk^+ + 1}} ``\dot \FQ$ is $\gk'$-directed closed
for $\gk'$ the least inaccessible cardinal greater than $\gk$'',
it suffices to show that the desired conclusions are true in $V^{\FP_{\gk^+ + 1}}$.
To do this, suppose first that trivial forcing is selected in the
stage $\gk^+$ lottery held in the definition of $\FP$. Because by our hypotheses on $V$,
$V \models ``$GCH + $\gk$ is a measurable
%$V \models ``\gk$ is a measurable
cardinal which carries $2^{2^{\gk}} = \gk^{++}$ many normal measures'',
it immediately follows that
$V^{\FP_{\gk^+ + 1}} = V^{\FP_{\gk^+}} \models ``\gk$
is a measurable cardinal which carries $2^{2^{\gk}} = \gk^{++} $
many normal measures'' as well.
Suppose now that ${\rm Coll}(\gk^+, \gk^{++})$ is selected in the
stage $\gk^+$ lottery held in the definition of $\FP$. Since
$\FP_{\gk^+ + 1}$ is forcing equivalent to
$\FP_{\gk^+} \ast \dot {\rm Coll}(\gk^+, \gk^{++})$ where
$\card{\FP_{\gk^+}} < \gk$ and $\FP_{\gk^+}$ is nontrivial, the proofs of \cite[Lemma 2.2]{A07}
and \cite[Lemma 2.5]{AF11} show that
$V^{\FP_{\gk^+ + 1}} \models ``\gk$ is a measurable cardinal
which carries $\gk^+$ many normal measures''.
This completes the proof of Lemma \ref{l5}.
\end{proof}
\begin{lemma}\label{l6}
$V^\FP \models ``\gk$ is a measurable cardinal which is not a limit
of measurable cardinals'' iff
$V \models ``\gk$ is a measurable cardinal which is not a limit of measurable cardinals''.
\end{lemma}
\begin{proof}
We use ideas found in the proof of \cite[Lemma 2.1]{A07}.
Suppose $V^\FP \models ``\gk$ is a measurable cardinal which is not a limit
of measurable cardinals''. By the factorization of $\FP$ given in Lemma \ref{l4}
and Theorem \ref{tgf}, $V \models ``\gk$ is a measurable cardinal'' as well. If
$V \models ``\gk$ is a measurable cardinal which is a limit of measurable cardinals'', then
$V \models ``\gk$ is a measurable cardinal which is a limit of measurable cardinals $\gd$,
each of which is not a limit of measurable cardinals''. By Lemma \ref{l5}, every such
%measurable cardinal
$\gd$ remains measurable in $V^\FP$. Thus,
$V^\FP \models ``\gk$ is a limit of measurable cardinals'', a contradiction.
This tells us that if
$V^\FP \models ``\gk$ is a measurable cardinal which is not a limit
of measurable cardinals'', then
$V \models ``\gk$ is a measurable cardinal which is not a limit of measurable cardinals''.
On the other hand, if
$V \models ``\gk$ is a measurable cardinal which is not a limit of measurable cardinals'',
the proof of Lemma \ref{l5} shows that
$V^\FP \models ``\gk$ is a measurable cardinal''.
Suppose $V^\FP \models ``\gk$ is a measurable
cardinal which is a limit of measurable cardinals''. Then as above,
the factorization of $\FP$ given in Lemma \ref{l4} and Theorem \ref{tgf} yield that
$V \models ``\gk$ is a measurable cardinal which is a limit of measurable cardinals'',
a contradiction.
Hence, if $V \models ``\gk$ is a measurable cardinal which is not a limit of measurable cardinal'', then
$V^\FP \models ``\gk$ is a measurable cardinal which is not a limit of measurable cardinals''.
This completes the proof of Lemma \ref{l6}.
\end{proof}
\begin{lemma}\label{l7}
$V^\FP \models ``V = {\rm HOD}$''.
\end{lemma}
\begin{proof}
By Lemma \ref{l6}, the measurable cardinals which are not limits of measurable
cardinals are precisely the same in both $V$ and $V^\FP$.
Lemma \ref{l5} therefore allows us to infer that if $V^\FP \models ``\gk$
is a measurable cardinal which is not a limit of measurable cardinals'', then in $V^\FP$,
$\gk$ carries either $2^{2^\gk}$ many normal measures or $\gk^+$ many normal measures,
depending on whether trivial forcing or ${\rm Coll}(\gk^+, \gk^{++})$ was
selected in the stage $\gk^+$ lottery held in the definition of $\FP$.
By hypothesis, we also know that $V$ contains a proper class of measurable cardinals,
Consequently, the same proof as given in Lemma \ref{l3}, with the coding oracle
``$\diamondsuit^*_{\gk^{++}}$ holds or fails for $\gk$ a singular cardinal'' replaced by
``Every measurable cardinal $\gk$ which is not a limit of measurable cardinals
carries either $2^{2^\gk}$ many normal measures or $\gk^+$ many normal measures'',
now shows that $V^\FP \models ``V = {\rm HOD}$''.
This completes the proof of Lemma \ref{l7}.
\end{proof}
\begin{lemma}\label{l8}
$V^\FP \models {\rm GA}$.
\end{lemma}
\begin{proof}
We follow the proofs of \cite[Theorem 4.7]{AF11} and \cite[Theorem 10]{R07}.
Let $V^\FP = \ov V$. Towards a contradiction, suppose
that $\ov V$ is a set forcing extension of an inner model
$W$ of ZFC. In particular, we assume that
$W \subseteq \ov V$ is such that $\ov V = W[h]$, where $h$ is
$W$-generic for some set partial ordering $ \FQ \in W$.
By the L\'evy-Solovay results \cite{LS}, for $\gk > \card{\FQ}$,
the models $W$ and $\ov V$ will
agree on the properties
``$ \gk $ is a measurable cardinal",
``$\gk $ carries $2^{2^\gk}$ many normal measures",
and ``$\gk$ carries $\gk^+$ many normal measures''.
Every set of ordinals $x \in \ov V$ is coded using the oracle
``Every measurable cardinal $\gk$ which is not a limit of measurable cardinals
carries either $2^{2^\gk}$ many normal measures or $\gk^+$ many normal measures''.
The claim is that one such code for $x$ must appear above $\card{\FQ}$.
If $p \forces ``\dot x \subseteq \ga$ and $\card{\dot \FQ} = \gep$'',
let $ \gep^*=\rm{max}(\ga,\gep) $.
The proof of Lemma \ref{l3}, with $\gep^*$ replacing $\ga$ in the definition of $\gd$ and
a term for trivial forcing and $\dot {\rm Coll}(\gs^+, \gs^{++})$ replacing
$\dot \FQ^\diamondsuit(\gs)$ and $\dot \add(\gs, \gs^+)$ respectively in the definition of $q_\gs$
at nontrivial stages of forcing $\gs$, then shows that
there is a dense set of conditions forcing that $x$ is coded above $\card{\FQ}$.
This means that the code also appears in $W$. %, i.e., $x \in W$.
Consequently $x \in W$,
and so every set of ordinals of $\ov V$ is also in $W$. This shows that $\ov V = W$, which means
that the forcing $\FQ$ was trivial. Thus, $V^\FP \models {\rm GA}$.
This completes the proof of Lemma \ref{l8}.
\end{proof}