\documentclass[11pt]{amsart}
\usepackage{amsmath,amssymb,amscd,amsthm,amsfonts,amstext,amsbsy,mathrsfs,hyperref,upgreek,mathtools,stmaryrd,enumitem,bbm}
%\usepackage{MnSymbol}
%\usepackage[shadow]{todonotes}
% \usepackage{citeref, breakcites}
\usepackage[german, english]{babel} 
\usepackage[textsize=footnotesize,color=blue!40, bordercolor=white]{todonotes}

\usepackage%[scale=0.682]
[a4paper, margin=1.2in]{geometry}

% other fonts
\newcommand\V{\mathsf{V}}
\newcommand{\Minimal}{\MM[\![G]\!]}
\newcommand\bB{\boldsymbol{{\rm B}}}
\newcommand\bN{\boldsymbol{{\rm N}}}
\renewcommand{\L}{\mathcal{L}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\M}{\mathcal{M}}
\newcommand{\T}{\mathcal{T}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\EE}{\mathbb{E}}                                                       
\newcommand{\OO}{\mathbb{O}}
\newcommand{\PP}{\mathbb{P}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\TT}{\mathbb{T}}
\newcommand{\KK}{\mathbb{K}}
\newcommand{\CC}{\mathbb{C}}
\newcommand{\BB}{\mathbb{B}}
\newcommand{\MM}{\mathbb{M}}
\newcommand{\HH}{\mathbb{H}}
\newcommand{\FF}{\mathbb{F}}
\newcommand{\Ss}{\mathbb{S}}
\newcommand{\HHH}[1]{\mathrm{H}({#1})}
\newcommand{\Hes}{\mathfrak{H}}
\newcommand{\pre}[2]{{}^{#1} #2}
\newcommand{\seq}[2]{\langle #1 \mid #2 \rangle}
\newcommand{\set}[2]{\{ #1 \mid #2 \}}
\newcommand{\Nbhd}{\mathbf{N}}
\newcommand{\Bor}{\mathsf{Bor}}
\newcommand{\pI}{\mathrm{I}}
\newcommand{\pII}{\mathrm{II}}
%\newcommand{\K}[1]{\boldsymbol{K}_{#1}}
\newcommand{\K}[1]{\mathrm{K}_{#1}}
\newcommand{\anf}[1]{{\text{``}\hspace{0.3ex}{#1}\hspace{0.01ex}\text{''}}}
\newcommand{\op}{\mathsf{op}}
\newcommand{\rnk}{\mathsf{rnk}}
\newcommand{\crnk}[2]{\mathsf{rnk}_{#1}(#2)}

% operators
\newcommand{\id}{\operatorname{id}}
\newcommand{\cof}{\operatorname{cof}}
\newcommand{\otp}[1]{{{\rm{otp}}\left(#1\right)}}
\newcommand{\supp}[1]{{{\rm{supp}}(#1)}}
\newcommand{\proj}{\operatorname{p}}
\newcommand{\pow}{\mathscr{P}}
\newcommand{\Trcl}{\operatorname{Trcl}}
\newcommand{\Mod}{\operatorname{Mod}}
\newcommand{\p}{\operatorname{p}}
\newcommand{\leng}{\operatorname{lh}}
\newcommand{\Fn}{\mathrm{Fn}}
\newcommand{\range}{\operatorname{range}}
\newcommand{\rank}{\operatorname{rank}}
\newcommand{\Col}{\operatorname{Col}}
\newcommand{\ra}{\rightarrow}
\newcommand{\lr}{\leftrightarrow}
\newcommand{\cf}{\mathrm{cf}}
\newcommand{\Llr}{\Longleftrightarrow}
\newcommand{\tc}{\operatorname{tc}}
\newcommand{\depth}{\operatorname{d}}
%\newcommand{\Add}{\operatorname{Add}}
\newcommand{\ul}{\ulcorner}
\newcommand{\ur}{\urcorner}
\newcommand{\lh}{\operatorname{lh}}
\newcommand{\llangle}{\langle\!\langle}
\newcommand{\rrangle}{\rangle\!\rangle}
\newcommand{\vn}{\vec{n}}
\newcommand{\one}{\mathbbm1}
\newcommand{\lkk}{\L_{\kappa,\kappa}}
\newcommand{\gbr}[1]{{\ulcorner{#1}\urcorner}}
\newcommand{\Def}{\mathrm{Def}}
\newcommand{\Card}{\mathrm{Card}}
% spaces
\newcommand{\On}{{\mathrm{Ord}}}
%\newcommand{\Card}{{\sf Card}}
\newcommand{\Lim}{{\mathrm{Lim}}}
\newcommand{\Fm}{{\mathrm{Fml}}}
%\newcommand{\Sym}{{\rm Sym}}
\newcommand{\push}{{\mathrm{push}}}


% axioms
\newcommand{\AD}{{\sf AD}}
\newcommand{\ZFC}{{\sf ZFC}}
\newcommand{\ZF}{{\sf ZF}}
\newcommand{\AC}{{\sf AC}}
\newcommand{\DC}{{\sf DC}}
\newcommand{\KM}{{\sf KM}}
\newcommand{\GB}{{\sf GB}}
\newcommand{\GBC}{{\sf GBC}}
\newcommand{\GCH}{{\sf GCH}}
\newcommand{\CH}{{\sf CH}}

% others
\newcommand{\Linf}{\L_{\omega_1 \omega}}

%Luecke
\newcommand{\map}[3]{{#1}:{#2}\longrightarrow{#3}}
\newcommand{\Map}[5]{{#1}:{#2}\longrightarrow{#3};~{#4}\longmapsto{#5}}
\newcommand{\pmap}[4]{{#1}:{#2}\xrightarrow{#4}{#3}}
\newcommand{\Set}[2]{\{{#1}~\vert~{#2}\}}
\newcommand{\ran}[1]{{{\rm{ran}}(#1)}}
\newcommand{\dom}[1]{{{\rm{dom}}(#1)}}
\newcommand{\length}[1]{{{\rm{lh}}(#1)}}
\newcommand{\VV}{{\rm{V}}}
\newcommand{\WW}{{\rm{W}}}
\newcommand{\LL}{{\rm{L}}}
\newcommand{\Add}[2]{{\rm{Add}}({#1},{#2})}
\newcommand{\goedel}[2]{{\prec}{#1},{#2}{\succ}}
\newcommand{\ot}{ot}

% theorems

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{question}[theorem]{Question}
\newtheorem{problem}[theorem]{Problem}
\newtheorem{observation}[theorem]{Observation}
\newtheorem{claim}{Claim}
\newtheorem*{claim*}{Claim}
\newtheorem*{subclaim*}{Subclaim}
\newtheorem*{Vaughtconj}{Vaught's Conjecture}
\theoremstyle{definition}
%\newtheorem{claim}{Claim}[theorem]
\newtheorem{definition}[theorem]{Definition}
\newtheorem*{notation}{Notation}
\newtheorem{fact}[theorem]{Fact}
\newtheorem{example}[theorem]{Example}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\setcounter{tocdepth}{1}

%\renewcommand{\thetheorem}{\arabic{theorem}}
\title{Class forcing}
\author{Regula Krapf}
\date{\today}

\begin{document}
 \maketitle
 
We have seen how to modify the continuum function $\kappa\mapsto2^\kappa$ by forcing both $\CH$ and $\neg\CH$. It would be interesting to force generalizations of this such as $\GCH$ or forcing $2^\kappa=\kappa^{++}$ for every regular cardinal. 
However, this is impossible, since every forcing $\PP$ satisfies the $|\PP|^+$-cc and therefore does not modify the continuum function above $\kappa$. To achieve this, we have to generalize forcing and allow \emph{proper class} partial orders. 
 
 \section{G\"odel-Bernays set theory}
 
Since we will now deal with classes, we will work in a second-order context. We work in a two-sorted version of $\L_\in$ with (lowercase letter) variables for sets and (capital letter) variables for classes. More precisely, the formulae are given by
\begin{itemize}
 \item atomic formulae of the form $v_i\in v_j,v_i=v_j, v_i\in W_j, W_i=W_j$
 \item if $\varphi,\psi$ are formulae then so are $\neg\varphi,\varphi\wedge\psi$
 \item if $\varphi$ is a formula then so are $\exists v_i\varphi,\exists W_i\varphi$.
\end{itemize}
By \emph{first-order formulae} we denote the formulae which have no class quantifiers (but classes may appear in atomic subformulae).

The theory $\GB$ consists of the \emph{set axioms} given by $\ZF$ (where in the schemes of Separation and Replacement formulae are allowed to have class parameters\footnote{e.g. for Separation this means: Whenever $\varphi(v_0,v_1,p_0,\dots,p_{m-1},C_0,\dots,C_{n-1})$ is an $\L_\in$-formula with set parameters $p_0,\dots,p_{m-1}$ and class parameters $C_0,\dots,C_{n-1}$ then $\{y\in x\mid\varphi(x,y,p_0,\dots,p_{m-1},C_0,\dots,C_{m-1})\}$ is a set.}) and the \emph{class axioms}
\begin{itemize}
 \item $\forall X,Y(X=Y\lr\forall z(z\in X\lr z\in Y)$ (\emph{Extensionality})
 \item $\forall X(X\neq\emptyset\ra\exists y\in X\forall z\in y(z\notin X))$ (\emph{Foundation})
 \item For every formula $\varphi$ without class quantifiers, $$\forall X_0,\dots,X_{n-1}\exists Y\forall z[z\in Y\lr\varphi(z,X_1,\dots,X_{n-1})]\quad\text{(\emph{first-order Class Comprehension})}$$ 
%  \item For every formula $\varphi$ without class quantifiers, \begin{align*}&\forall X_0,\dots,X_{n-1}\forall Y[\forall y\in Y\exists!z\varphi(y,z,X_0,\dots,X_{n-1})\ra\\&\exists Z\forall z(z\in Z\lr\exists y\in Y\,\varphi(y,z,X_0,\dots,X_{n-1}))]\quad\text{(\emph{Replacement})}\end{align*} 
\end{itemize}
Furthermore, we denote by $\GBC$ the theory of $\GB$ enhanced by \emph{global choice}, i.e.
$$\exists F[F\text{ function }\wedge\forall x\neq\emptyset(x\in\dom{F}\wedge F(x)\in x)].$$
As in the case of $\ZFC$, we write $\GB(\mathsf C)^-$ for the theory $\GB(\mathsf C)$ without the power set axiom.\\[0.2cm]
A model of $\GBC$ (or one of the weaker subtheories) is of the form $\MM=\langle M,\C\rangle$ where $M$ contains the sets and $\C$ contains the classes. 

\begin{remark}
 If $M$ is a transitive model of $\ZFC$ and $\Def(M)$ denotes the collection of classes which are definable over $M$ then $\langle M,\Def(M)\rangle\models\GB$. This shows that $\GBC$ is \emph{conservative} over $\ZFC$, i.e. every statement that $\GBC$ proves about sets can also be proven in $\ZFC$. 
\end{remark}

 
 \section{Class forcing}
% Let $M$ be a (countable) transitive model of $\ZFC$. Recall that a \emph{class} $C$ of $M$ is a subset of $M$ which is definable over $M$, i.e. there is an $\L_\in$-formula $\varphi$ and a parameter $x\in M$ such that
% $$C=\{y\in M\mid\varphi(y,x)\}.$$
% 
% We will now work in a second-order context with models of the form $\langle M,\Def(M)\rangle$. 
Let $\MM=\langle M,\C\rangle$ be a model of $\GB$. 
 
\begin{definition}
A \emph{class forcing} for $\MM$ is a triple of the form $\PP=\langle P,\leq_\PP,\one_\PP\rangle$ where $P,\leq_\PP\in\C$\footnote{We will usually identify $\PP$ with its domain $P$.}. 
A class $D\subseteq\PP$ is said to be
\begin{itemize}
 \item \emph{dense}, if for every $p\in\PP$ there is $q\leq_\PP p$ with $q\in D$.
 \item \emph{dense below $p$} for some $p\in\PP$, if for every $q\leq_\PP p$ there is $r\leq_\PP q$ with $r\in D$.
 \item \emph{predense}, if for every $p\in\PP$ there is $q\in D$ such that $p$ and $q$ are compatible.
 \item \emph{predense below $p$} for some $p\in\PP$, if for every $q\leq_\PP p$ there is $r\in D$ which is compatible with $q$. 
\end{itemize}
A filter $G\subseteq\PP$ is \emph{$\MM$-generic for $\PP$}, if $G\cap D\neq\emptyset$ for each dense class $D\in\C$. 
\end{definition}

\begin{lemma}Let $\PP$ be a class forcing for $\MM$ and $G\subseteq\PP$ a filter. Then the following statements are equivalent: 
\begin{enumerate}
 \item $G$ is $\MM$-generic for $\PP$.
 \item $G\cap D\neq\emptyset$ for every class $D\subseteq\PP$ in $\C$ which is dense below som e$p\in\PP$.
 \item $G\cap D\neq\emptyset$ for every predense class $D\subseteq\PP$ which is in $\C$.
 \item $G\cap D\neq\emptyset$ for every class $D\subseteq\PP$ in $\C$ which is predense below some $p\in G$.
\end{enumerate}
\end{lemma}

\begin{proof}The equivalence of (1) and (2) is shown in Problem 11, Models of Set Theory I. 
We show first that (1) $\Rightarrow$ (3). Let $D\subseteq\PP$ be a predense class in $\C$. Then consider $$\bar D=\{p\in\PP\mid\exists q\in D(p\leq_\PP q)\}.$$
We check that $\bar D$ is dense. Let $p\in\PP$. Then there is $q\in D$ which is compatible with $p$. Take $r\leq_\PP p,q$. Then $r\in\bar D$, so $\bar D$ is dense. 
Pick $p\in G\cap\bar D$ and $q\in D$ with $p\leq_\PP q$. Then $q\in G\cap D$.

Suppose now that (3) holds and let $p\in G$ and $D\subseteq\PP$ be predense below $p$. Then $$\bar D=D\cup\{q\in\PP\mid q\bot_\PP p\}$$ is predense, so we can pick $q\in G\cap\bar D$. But then $p,q$ are compatible, so $q\in G\cap D$.

The implication (4) $\Rightarrow$ (1) is obvious. 
\end{proof}

\begin{definition}Let $\PP$ be a class forcing for $\MM$. 
A \emph{$\PP$-name} is a class whose elements are of the form $\langle\sigma,p\rangle$ where $\sigma$ is a $\PP$-name and $p\in\PP$. We define $M^\PP$ to be the class of all $\PP$-names which are elements of $M$ and $\C^\PP$ the collection of $\PP$-names which are in $\C$ (denoted \emph{class $\PP$-names}).

Given an $\MM$-generic filter $G$ for $\PP$ and $\sigma\in M^\PP$, we define
$$\sigma^G=\{\tau^G\mid\exists p\in G(\langle\tau,p\rangle\in\sigma)\}$$
and similarly we define $\Gamma^G$ for $\Gamma\in\C^\PP$. Furthermore, let
\begin{align*}
 M[G]&=\{\sigma^G\mid\sigma\in M^\PP\}\\
 \C[G]&=\{\Gamma^G\mid\Gamma\in\C^\PP\}
\end{align*}
and $\MM[G]=\langle M[G],\C[G]\rangle$. 
\end{definition}

% If $G$ is $\MM$-generic for $\PP$ then $G$ is, in general, a proper class. In order to make reference to $G$ and other class names, we have to slightly generalize the axiom schemes of Separation and Replacement. If $\langle M,\in,R_0,\dots,R_{n-1}\rangle$ is a model with predicates $R_i\subseteq M$, then we say that $\langle M,\in,R_0,\dots,R_{n-1}\rangle$ satisfies Separation (resp. Replacement), if it satisfies Separation (Replacement) for $\L_\in$-formulae which allow $R_0,\dots,R_{n-1}$ as predicates. In particular, we say that $\langle M,\in,R_0,\dots,R_{n-1}\rangle\models\ZFC$ if $\langle M,\in\rangle$ is a model of $\ZFC$ and $\langle M,\in,R_0,\dots,R_{n-1}\rangle$ satisfies Separation and Replacement. 
% 
% Note that if $C_0,\dots,C_{n-1}\in\Def(M)$ then $\langle M,\in,C_0,\dots,C_{n-1}\rangle\models\ZFC$.

\begin{definition}
 %If $\varphi(x_0,\dots,x_{m-1},C_0,\dots,C_{n-1})$ is an $\L_\in$-formula with $n$ class parameters, 
 If $\varphi\equiv\varphi(v_0,\ldots,v_{m-1},\Gamma_0,\ldots,\Gamma_{n-1})$ is an $\L_\in$-formula with class name parameters $\Gamma_0,\dots,\Gamma_{n-1}\in\C^\PP$, 
 $p\in\PP$ and $\sigma_0,\dots,\sigma_{m-1}\in M^\PP$, we write $$p\Vdash_\PP^\MM\varphi(\sigma_0,\dots,\sigma_{m-1},\Gamma_0,\dots,\Gamma_{n-1})$$
 if for $\MM$-generic filter $G$ for $\PP$ with $p\in G$, $$\MM[G]\models\varphi(\sigma_0^G,\dots,\sigma_{m-1}^G,\Gamma_0^G,\dots,\Gamma_{n-1}^G).$$ 
% We say that $M[G]$ satisfies $\ZFC$ (or similarly for some weaker subtheory of $\ZFC$), if $\langle M[G],\Gamma_0^G,\dots,\Gamma_{m-1}^G\rangle\models\ZFC$ for all class $\PP$-names $\Gamma_0,\dots,\Gamma_{n-1}$. 
\end{definition}

\begin{definition}\label{def:ft}Let $\MM$ be a model of $\GB$. 
 Let $\varphi\equiv\varphi(v_0,\ldots,v_{m-1},\Gamma_0,\ldots,\Gamma_{n-1})$ be an $\L_\in$-formula with class name parameters $\Gamma_0,\dots,\Gamma_{n-1}\in\C^\PP$. 
 \begin{enumerate}
  \item We say that \emph{$\PP$ satisfies the definability lemma for $\varphi$ over $\MM$} if 
   \begin{equation*}
  \Set{\langle p,\sigma_0,\ldots,\sigma_{m-1}\rangle\in P\times M^\PP\times\ldots\times M^\PP}{p\Vdash^\MM_\PP\varphi(\sigma_0,\ldots,\sigma_{m-1},\Gamma_0,\ldots,\Gamma_{n-1})}\in\C. 
 \end{equation*} 
 \item We say that \emph{$\PP$ satisfies the truth lemma for $\varphi$ over $\MM$} if for all $\sigma_0,\ldots,\sigma_{m-1}\in M^\PP$, $\vec{\Gamma}\in(\C^\PP)^n$ and every filter $G$ which is $\PP$-generic over $\MM$ with 
  \begin{equation*}
    \MM[G]\models\varphi(\sigma_0^G,\ldots,\sigma_{m-1}^G,\Gamma_0^G,\dots,\Gamma_{n-1}^G), 
  \end{equation*}
  there is $p\in G$ with $p\Vdash^{\MM}_\PP\varphi(\sigma_0,\ldots,\sigma_{m-1},\Gamma_0,\ldots,\Gamma_{n-1})$.
  \item We say that \emph{$\PP$ satisfies the forcing theorem for $\varphi$ over $\MM$} if $\PP$ satisfies both the definability lemma and the truth lemma for $\varphi$ over $\MM$.
 \end{enumerate}
 \end{definition}
 
\begin{question}
Is it true that if $M\models\GB$ and $\PP$ is a class forcing for $M$ then $M[G]\models\GB$ whenever $G$ is $\MM$-generic for $\PP$? A related question is: Does every class forcing satisfy the forcing theorem?
\end{question}

The answer is that, in general, the axioms of set theory are not preserved under class forcing (see e.g. Problem 29). Moreover, there are class forcings for which the forcing theorem fails. 
Before we proceed to more technical results, let us consider an easy application of class forcing.

\begin{definition}
 A class forcing $\PP$ is \emph{$<\On$-closed}, if for every cardinal $\kappa$ and for every descending sequence $\langle p_\alpha\mid\alpha<\kappa\rangle$ there is $p\in\PP$ with $p\leq_\PP p_\alpha$ for each $\alpha<\kappa$. 
\end{definition}

\begin{lemma}\label{lemma:<-On-closed sdp}
 Let $\PP$ be a class forcing which is $<\On$-closed. Then the following statements hold:
 \begin{enumerate}
  \item If $G$ is $\MM$-generic for $\PP$ then $M[G]=M$. 
  \item $\PP$ preserves the axioms of $\GB$ (resp. $\GB+\AC$ or $\GBC$).
 \end{enumerate}
\end{lemma}

\begin{proof}
 This follows from Problem 28.
\end{proof}

% \begin{lemma}
% Let $\PP$ be $<\On$-closed. Then 
% \end{lemma}
% 
% \begin{proof}
% This follows from Lemma \ref{lemma:<On-closed pretame} and Lemma \ref{lemma:<-On-closed sdp}.
% \end{proof}


\begin{definition}
 A \emph{global well-order} for $M$ is a class well-order $\prec\,\in\C$ of $M$. Note that by Problem 27 the existence of a global well-order for $M$ is equivalent to \emph{global choice}.
\end{definition}

\begin{proposition}
There is a class forcing $\PP$ which adds a global well-order for $M$. More precisely, if $\MM\models\GB+\mathsf{AC}$ and $G$ is $\MM$-generic for $\PP$ then $\MM[G]\models\GBC$.
\end{proposition}

\begin{proof}
Let $\PP=\{\prec\,\in M\mid\exists x\in M(\prec\text{ is a well-order of }x)\}$, ordered by end-extension, i.e. if $p,q\in\PP$ then $p\leq_\PP q$ if and only if $\dom{p}\supseteq\dom{q}$ and $p\upharpoonright\dom{q}\times\dom{q}=q$, where $\dom{p}$ is the set well-ordered by $p$.
Note that $\PP$ is $<\On$-closed, so $M[G]=M$ and $\MM[G]\models\GB$.

Let $G$ be $\MM$-generic for $\PP$ and consider $\prec\,=\bigcup G$. For each $x\in M$ consider 
$$D_x=\{p\in\PP\mid x\subseteq\dom{p}\}.$$
We show that $D_x$ is dense. Let $p\in\PP$ and $y=\dom{p}$. Let $z=x\setminus y$ and let $q$ be a well-order of $z$. Then there is a well-order $r\in\PP$ of $x\cup y$ given by
\begin{align*}
 \langle a,b\rangle\in r\Llr(a,b\in y\wedge\langle a,b\rangle\in p)\vee(a,b\in z\wedge\langle a,b\rangle\in q)\vee(a\in y\wedge b\in z).
\end{align*}
Then $r\leq_\PP p$ and $r\in D_x$.

To see that $\prec$ is an ordering of $M$, let $x\in M$ be arbitary and pick $p\in D_{\{x\}}$. Hence $x\in\dom{p}\subseteq\dom{\prec}$. We show that it well-orders $M$. To see that it is a linear ordering, let $x,y\in M$. Take $p\in G\cap D_{\{x,y\}}$. Then either $\langle x,y\rangle\in p$ or $\langle y,x\rangle\in p$. In the first case, $x\prec y$ and in the second case, $y\prec x$. Moreover, $\prec$ is a well-order: We have to check that for every $x\in M$, $x$ has a $\prec$-least element. 
Pick $p\in G\cap D_x$. Then $\prec\upharpoonright\dom{p}\times\dom{p}=p$ is a well-order on $\dom{p}\supseteq x$. But then $x$ has a $p$-least element $y$ and in particular $y$ is also a $\prec$-least element of $x$.  
\end{proof}



% \begin{proof}[Proof]Let $\sigma\in M^\PP$ be a $\PP$-name. 
% We prove that the set $$D_\sigma=\{p\in\PP\mid\exists x\in M(p\Vdash_\PP^\MM\sigma=\check x)\}$$ is dense. 
% By induction, we may assume that for each $\tau\in\dom{\sigma}$, $D_\tau$ is dense. 
% 
% Let $p\in\PP$ be an arbitary condition.
% Now let $\langle\tau_\alpha\mid\alpha<\kappa\rangle$ be an enumeration of $\dom{\sigma}$. We recursively construct a descending sequence $\langle p_\alpha\mid\alpha<\kappa\rangle$ of conditions in $G$ and $\langle x_\alpha\mid\alpha<\kappa\rangle$ of sets in $M$. 
% \begin{itemize}
%  \item Let $p_0=p$.
%  \item Given $p_\alpha$ for some $\alpha<\kappa$, if $p_{\alpha+1}\nVdash_\PP\tau_\alpha\notin\sigma$ then let $\bar p_\alpha\leq_\PP p_\alpha$ with $\bar p_\alpha\Vdash_\PP^\MM\tau_\alpha\in\sigma$. Now
%  let $p_{\alpha+1}\leq_\PP\bar p_\alpha$ be in $D_{\tau_\alpha}$ and $x_\alpha\in M$ such that $p_{\alpha+1}\Vdash_\PP^\MM\tau_\alpha=\check x_\alpha$. Otherwise, let $x_\alpha=\emptyset$. 
%  \item If $\alpha<\kappa$ is a limit ordinal, let $p_\alpha\in\PP$ with $p_\alpha\leq_\PP p_\beta$ for each $\beta<\alpha$, using that $\PP$ is $<\On$-closed.
% \end{itemize}
% Finally, let $q\in\PP$ with $q\leq_\PP p_\alpha$ for each $\alpha<\kappa$. Put $x=\{x_\alpha\mid \alpha<\kappa\wedge p_{\alpha+1}\Vdash_\PP^\MM\tau_\alpha\in\sigma\}$. Then $q\Vdash_\PP^\MM\sigma=\check x$, so $q\in D_\sigma$. 
%\end{proof}

\section{Pretameness}

% \begin{definition}
% Let $\PP$ be a class forcing. A class $D\subseteq\PP$ is said to be \emph{predense (below $p\in\PP$)}, if every $q\in\PP$ (resp. every $q\leq_\PP p$) is compatible with some element of $D$. 
% \end{definition}
Since fundamental theorems of set forcing such as the forcing theorem and the preservation of the axioms of set theory can fail for class forcing, we are interested in finding a condition which guarantees that at least $\GB^-$ is preserved and the forcing theorem holds. 

\begin{definition}Let $\PP$ be a class forcing for $\MM$. We say that $\PP$ is \emph{pretame}, if for every sequence of dense (below $p$) classes $\langle D_\alpha\mid\alpha<\kappa\rangle$ in $\C$ (i.e. $\{\langle p,\alpha\rangle\mid p\in D_\alpha\}\in\C$) and for every $p\in\PP$ there is a sequence $\langle d_\alpha\mid\alpha<\kappa\rangle\in M$ and $q\leq_\PP p$ such that each $d_\alpha\subseteq D_\alpha$ is predense below $q$. 
\end{definition}

\begin{remark}
 Note that if $M\models\AC$ then we can always assume $I$ to be a cardinal in the above definition.
\end{remark}


\begin{proposition}[S. Friedman]
 If $\PP$ is pretame then $\PP$ satisfies the forcing theorem.
\end{proposition}

\begin{proof}
 We have to show that $p\Vdash_\PP^\MM\sigma\in\tau$ and $p\Vdash_\PP^\MM\sigma=\tau$ are definable, since the definability of non-atomic formulae follows by induction on the formula complexity. We will define a class function $F:\PP\times M^\PP\times M^\PP\times2\ra 2\times M\setminus\{\emptyset\}$. 

We will prove by induction that $F(p,\sigma,\tau,0)=\langle i,d\rangle$ for some $d\subseteq\{q\in\PP\mid q\leq_\PP p\}$ such that either
\begin{itemize}
 \item[(1)] $i=1$ and for every $q\in d$, $q\Vdash_\PP^\MM\sigma\in\tau$, or
 \item[(2)] $i=0$ and for every $q\in d$, $q\Vdash_\PP^\MM\sigma\notin\tau$;
\end{itemize}
and similarly $F(p,\sigma,\tau,1)=\langle i,d\rangle$ for some $d\subseteq\{q\in\PP\mid q\leq_\PP p\}$ such that either
\begin{itemize}
 \item[(3)] $i=1$ and for every $q\in d$, $q\Vdash_\PP^\MM\sigma=\tau$, or
 \item[(4)] $i=0$ and for every $q\in d$, $q\Vdash_\PP^\MM\sigma\neq\tau$.
\end{itemize}
Given such a function, we can define the forcing relation by
 \begin{align*}
 p\Vdash_\PP^\MM\sigma\in\tau&\Llr\forall q\leq_\PP p\,\exists d\in M(F(q,\sigma,\tau,0)=\langle1,d\rangle)\\
 p\Vdash_\PP^\MM\sigma=\tau&\Llr\forall q\leq_\PP p\,\exists d\in M(F(q,\sigma,\tau,1)=\langle1,d\rangle).
 \end{align*}
We are left with defining such a function $F$ by induction on the name rank. We start with defining $F(p,\sigma,\tau,0)$.
By induction, we may assume that for all $\pi\in\dom{\tau}$ and for all $q\in\PP$, $F(q,\sigma,\pi,1)$ has already been defined. There are two cases:
\begin{itemize}
 \item[\emph{Case 1.}] There exist $\langle\pi,r\rangle\in\tau$ and $q\leq_\PP p,r$ such that $F(q,\sigma,\pi,1)=\langle1,d\rangle$ for some $d\in M$. Let $\alpha\in\On$ be minimal such that there is such a $d\in\V_\alpha$. Then put $F(p,\sigma,\tau,0)=\langle1,e\rangle$ where 
 $$e=\bigcup\{d\in\V_\alpha\mid\exists\langle\pi,r\rangle\in\tau\,\exists q\leq_\PP p,r\,F(q,\sigma,\pi,1)=\langle1,d\rangle\}.$$
 \item[\emph{Case 2.}] Suppose that Case 1 fails. For each $\langle\pi,r\rangle\in\tau$, consider
 $$D_{\pi,r}=\bigcup\{d\in M\mid\exists q\leq_\PP r\,F(q,\sigma,\pi,1)=\langle0,d\rangle\}\cup\{q\leq_\PP p\mid q\bot_\PP r\}.$$
 We show that $D_{\pi,r}$ is dense below $p$. Let $q\leq_\PP p$. If $q\bot_\PP r$ then we are done. Otherwise take $s\leq_\PP q,r$. Since Case 1 fails, $F(s,\sigma,\pi,1)=\langle0,d\rangle$ for some $d\in M\setminus\{\emptyset\}$. Since $d$ is nonempty, take $t\in d$. Then $t\in D_{\pi,r}$ and $t\leq_\PP s\leq_\PP q$. By pretameness there are conditions $q\leq_\PP p$ and $\langle d_{\pi,r}\mid\langle\pi,r\rangle\in\tau\rangle\in M$ such that each $d_{\pi,r}$ is a subset of $D_{\pi,r}$ which is predense below $q$. Now let $\alpha\in\On$ be minimal such that there is such $q$ in $\V_\alpha$. Then put $F(p,\sigma,\tau,0)=\langle0,e\rangle$ where 
 $$\qquad\quad e=\{q\in\V_\alpha\cap\PP\mid\exists\langle d_{\pi,r}\mid\langle\pi,r\rangle\in\tau\rangle\in M(d_{\pi,r}\text{ predense subset of }D_{\pi,r}\text{ below }q)\}.$$
\end{itemize}
% We show that $F$ satisfies (1). Suppose first that $p\Vdash_\PP^\MM\sigma\in\tau$ and let $q\leq_\PP p$. Assume, towards a contradiction, that $F(q,\sigma,\tau,0)=\langle0,d\rangle$ for some nonempty $d\in M$. Now let $s\in d$. Then there is a sequence $\langle d_{\pi,r}\mid\langle\pi,r\rangle\in\tau\rangle\in M$ of sets $d_{\pi,r}\subseteq D_{\pi,r}$ which are predense below $s$. Now if $G$ is $\MM$-generic with $s\in G$ then $M[G]\models\sigma^G\in\tau^G$ so there is $\langle\pi,r\rangle\in\tau$ with $r\in G$ and $M[G]\models\sigma^G=\pi^G$. Since $d_{\pi,r}$ is predense below $s$ there is $t\in d_{\pi,r}\cap G$. But then $t$ is compatible with $r$ and so there is $u\leq_\PP p$ with $F(u,\sigma,\pi,1)=\langle0,d\rangle$ for some $d$ with $t\in d$. Then $t\leq_\PP u$ and so $u\in G$. But by induction we have $t\Vdash_\PP^\MM\sigma\neq\pi$, a contradiction. 
We are left with checking (1) and (2). 
Suppose that $F(p,\sigma,\tau,0)=\langle1,e\rangle$. We have to check that for every $q\in e$, $q\Vdash_\PP^\MM\sigma\in\tau$. Take $q\in d$ and an $\MM$-generic filter $G$ with $q\in G$. Since we are in Case 1, there is $\langle\pi,r\rangle\in\tau$ and $s\leq_\PP p,r$ with $F(s,\sigma,\pi,1)=\langle1,d\rangle$ for some $d$ and $q\in d$. Then $q\leq_\PP s$ and so $s\in G$. But by induction, since $\rank(\pi)<\rank(\tau)$, $q\Vdash_\PP^\MM\sigma=\pi$ and so $\sigma^G=\pi^G\in\tau^G$.

Secondly, assume that $F(p,\sigma,\tau,0)=\langle0,e\rangle$ and let $q\in e$ and $G$ an $\MM$-generic filter for $\PP$. Now by Case 2 there is a sequence $\langle d_{\pi,r}\mid\langle\pi,r\rangle\in\tau\rangle$ of sets $d_{\pi,r}\subseteq D_{\pi,r}$ which are predense below $q$. Suppose for a contradiction that $M[G]\models\sigma^G\in\tau^G$. Then there is $\langle\pi,r\rangle\in\tau$ with $r\in G$ and $\sigma^G=\pi^G$. Since $d_{\pi,r}$ is predense below $q$ there is $s\in d_{\pi,r}\cap G$. Then $s$ is compatible with $r$ and so there are $d\in M$ and $t\leq_\PP r$ with $F(t,\sigma,\pi,1)=\langle0,d\rangle$ and $s\in d$. By induction, $s\Vdash_\PP^\MM\sigma\neq\pi$, contradicting that $\sigma^G=\pi^G$.

Now we define $F(p,\sigma,\tau,1)$. Again, we may assume that for every $\pi\in\dom{\sigma\cup\tau}$ and for every $q\in\PP$, $F(q,\pi,\sigma,0)$ and $F(q,\pi,\tau,0)$ have already been defined. As above, me make a case distinction:
\begin{itemize}
 \item[\emph{Case 1.}] There exist $\langle\pi,r\rangle\in\sigma\cup\tau$, $q\leq_\PP p,r, i\in2,d,e\in M$ and $s\in d$ such that $F(q,\pi,\sigma,0)=\langle i,d\rangle$ and $F(s,\pi,\tau,0)=\langle1-i,e\rangle$. Then let $\alpha\in\On$ be minimal with the property that such $e$ as above exists in $\V_\alpha$. Then put $F(p,\sigma,\tau,1)=\langle0,f\rangle$, where
 \begin{align*}f=\bigcup\{&e\in\V_\alpha\mid\exists\langle\pi,r\rangle\in\sigma\cup\tau\,\exists q\leq_\PP p,r\,\exists i\in 2\,\exists d\in M\,\exists s\in d\\&(F(q,\pi,\sigma,0)=\langle i,d\rangle\wedge F(s,\pi,\tau,0)=\langle1-i,e\rangle)\}.\end{align*}
 \item[\emph{Case 2.}] Suppose that Case 1 fails. For each $\langle\pi,r\rangle\in\sigma\cup\tau$ let 
 \begin{align*}
  D_{\pi,r}=\bigcup&\{e\mid\exists q\leq_\PP r\,\exists i\in2\,\exists d\,\exists s\in d(F(q,\pi,\sigma,0)=\langle i,d\rangle\wedge F(s,\pi,\tau,0)=\langle i,e\rangle\}\\&\cup\{q\in\PP\mid q\bot_\PP r\}.
 \end{align*}
Since Case 1 fails, each $D_{\pi,r}$ is dense below $p$. By pretameness there are conditions $q\leq_\PP p$ and $\langle d_{\pi,r}\mid\langle\pi,r\rangle\in\sigma\cup\tau\rangle\in M$ such that each $d_{\pi,r}$ is a subset of $D_{\pi,r}$ which is predense below $q$. Now let $\alpha\in\On$ be minimal such that there is such $q$ in $\V_\alpha$. Then put $F(p,\sigma,\tau,0)=\langle1,f\rangle$ where 
 $$\qquad\quad f=\{q\in\V_\alpha\cap\PP\mid\exists\langle d_{\pi,r}\mid\langle\pi,r\rangle\in\sigma\cup\tau\rangle\in M(d_{\pi,r}\text{ predense subset of }D_{\pi,r}\text{ below }q)\}.$$ 
\end{itemize}
It remains to check (3) and (4). Suppose first that $F(p,\sigma,\tau,1)=\langle1,f\rangle$ and let $q\in f$. Since we are in Case 2, this means that there is a sequence $\langle d_{\pi,r}\mid\langle\pi,r\rangle\in\sigma\cup\tau\rangle\in M$ such that each $d_{\pi,r}$ is a subset of $D_{\pi,r}$ which is predense below $q$. Now let $G$ be $\MM$-generic for $\PP$ with $q\in G$. Suppose that $\sigma^G\neq\tau^G$. Then there is $\langle\pi,r\rangle\in\sigma\cup\tau$ such that $r\in G$ and either $\pi^G\in\sigma^G\setminus\tau^G$ or $\pi^G\in\tau^G\setminus\sigma^G$. Without loss of generality, we may assume the former. Now by predensity of $d_{\pi,r}$ there is $s\in d_{\pi,r}\cap G\subseteq D_{\pi,r}\cap G$. But then by definition of $D_{\pi,r}$ there are $d,e\in M,i\in2$ and $t\leq_\PP r$ and $u\in d$ such that $F(t,\pi,\sigma,0)=\langle i,d\rangle$ and $F(u,\pi,\tau,0)=\langle i,e\rangle$ and $s\in e$. If $i=0$ then, since $s\in e$, $s\Vdash_\PP^\MM\pi\notin\sigma$ and so $\pi^G\notin\sigma^G$, a contradiction. Otherwise, since $s\in e$, $s\leq_\PP u$ and so $u\in G$. But $u\in d$ and so $u\leq_\PP t$ and in particular, $t\in G$. Moreover, by induction we have $t\Vdash_\PP^\MM\pi\in\tau$ and therefore $\pi^G\in\tau^G$ contradicting our assumption.

For (4), suppose that $F(p,\sigma,\tau,1)=\langle0,f\rangle$ and $q\in f$. Then we are in Case 1, and so there are $\langle\pi,r\in\sigma\cup\tau,s\leq_\PP p,r,i\in2,d,e\in M$ and $t\in d$ such that $F(s,\pi,\sigma,0)=\langle i,d\rangle$ and $F(t,\pi,\tau,0)=\langle1-i,e\rangle$ and $q\in e$. Let $G$ be $\MM$-generic for $\PP$ with $q\in G$. Suppose first that $i=1$. Then $q\Vdash_\PP^\MM\pi\notin\tau$ and so $\pi^G\notin\tau^G$.
Since $q\in e$, $q\leq_\PP t$ and so $t\in G$. But $t\in d$ and so $t\Vdash_\PP^\MM\pi\in\sigma$, hence $\pi^G\in\sigma^G$. In particular, $\sigma^G\neq\tau^G$ as desired. The case that $i=0$ is similar. 
% The construction for $F(p,\sigma,\tau,1)$ is similar. 

We now define the forcing relation for atomic formulae containing classes. 
We claim that $p\Vdash_\PP^\MM\sigma\in\Gamma$ if and only if the class 
$$D=\{q\leq_\PP p\mid\exists\langle\tau,r\rangle\in\Gamma(q\leq_\PP r\wedge q\Vdash_\PP^\MM\sigma=\tau)\}\in\C$$ is dense below $p$. Suppose first that $p\Vdash_\PP^\MM\sigma\in\Gamma$ and let $q\leq_\PP p$. Take an $\MM$-generic filter $G$ for $\PP$ with $q\in G$. Then $p\in G$ and so $\sigma^G\in\Gamma^G$. Let $\langle\pi,r\rangle\in\Gamma$ such that $r\in G$ and $\sigma^G=\pi^G$. Since $G$ is a filter, $q$ and $r$ are compatible and therefore there is $s\leq_\PP q,r$ with $s\in G$. In particular, $s\in D$. Conversely, suppose that $G$ is $\MM$-generic for $\PP$ with $p\in G$. By genericity, we can take $q\in D\cap G$. But then there is $\langle\pi,r\rangle\in\Gamma$ such that $q\leq_\PP r$. Hence $r\in G$ and so $\sigma^G=\tau^G\in\Gamma^G$. 

Finally, we define $p\Vdash_\PP^\MM\Gamma=\Pi$ for class $\PP$-names $\Gamma,\Pi$. But this is equivalent to stipulating that for all $\langle\sigma,s\rangle\in\Gamma$ and for all $\langle\tau,t\rangle\in\Pi$ and for all $q\leq_\PP p,s$ and for all $r\leq_\PP r,t$ there are $\bar q\leq_\PP q$ and $\bar r\leq_\PP r$ such that $\bar q\Vdash_\PP^\MM\sigma\in\Pi$ and $\bar r\Vdash_\PP^\MM\tau\in\Gamma$. 

This shows that the definability lemma holds for atomic formulae. For composite formulae, we can proceed by induction on the formula complexity, since at every step only finitely many new quantifiers are added. 
The truth lemma follows from the definability lemma as in set forcing. 
\end{proof}

\begin{remark}
Problem 29 shows that the converse is false. However, there are class forcings which do not satisfy the forcing theorem. Moreover, if $\PP$ is non-pretame then there is a class forcing $\QQ$ and a dense embedding $\PP\ra\QQ$ such that $\QQ$ does not satisfy the forcing theorem. 
\end{remark}

% \begin{lemma}\label{lemma:<On-closed pretame}
%  Every $<\On$-closed class forcing is pretame.\hfill\qedsymbol
% \end{lemma}
% 
% \begin{proof}
%  Let $\langle D_i\mid i<\kappa\rangle$ be a sequence of dense classes in $\C$ and $p\in\PP$. We define a decreasing sequence $\langle p_i\mid i<\kappa\rangle$ below $p$. Let $p_0=p$. Given $p_i$, let $p_{i+1}\leq_\PP p_i$ with $p_{i+1}\in D_i$. For $i<\kappa$ limit, pick $p_i\leq_\PP p_j$ for all $j<i$, using that $\PP$ is $<\On$-closed. Finally, let $q\leq_\PP p_i$ for all $i<\kappa$. Then $d_i=\{p_{i+1}\}$ is predense below $q$. 
% \end{proof}


\begin{proposition}
If $\PP$ is pretame and $G$ is $\MM$-generic for $\PP$ then $\MM[G]\models\GB^-$. If $\MM$ is a model of global choice then so is $\MM[G]$.
\end{proposition}

\end{document}