I recently finished reading a series of excellent articles by Peter Holy, Regula Krapf, Philipp Lücke, Ana Njegomir and Philipp Schlicht investigating properties of class forcing over models of ${\rm GBC}$ (Gödel-Bernays set theory). So I would like to summarize their results in this post. The bad news is that most crucial properties of set forcing that we rely on in forcing constructions can fail for a class forcing notion in a model of ${\rm GBC}$. There are some good news too. It turns out that most desirable properties in class forcing are equivalent either to *pretameness* or the ${\rm ORD}$-cc. A forcing notion has the ${\rm ORD}$-cc if all its antichains are sets. A forcing notion $\mathbb P$ is *pretame* if for every set-sized collection of dense classes $\{D_i\mid i\in I\}$ ($I$ a set) and every $p\in\mathbb P$, there is $q\leq p$ and sets $d_i\subseteq D_i$ for $i\in I$ such that each $d_i$ is predense below $q$. Pretame forcing notions are precisely the ones that preserve ${\rm GBC}^-$ (Gödel-Bernays without the powerset axiom) to a forcing extension (see [1]). It is easy to come up with an example of class forcing which doesn’t preserve ${\rm GBC}^-$, for instance take ${\rm Coll}(\omega,{\rm ORD})$ whose conditions are partial finite functions from $\omega$ to ${\rm ORD}$ ordered by inclusion. (The smaller class of *tame* forcing notions preserves full ${\rm GBC}$ over models of ${\rm GBC}$ and ${\rm KM}$ over models of ${\rm KM}$.) We can also eliminate many of the pathologies of class forcing by strengthening the base theory from ${\rm GBC}$ to say ${\rm KM}$ (Kelley-Morse set theory).

There are many philosophical debates (e.g., *multiverse view* versus *universe view*) about the meta-mathematical interpretation of set forcing. The two standard ways of resolving the difficulty that generic filters exist outside the set theoretic universe are the *countable transitive models* approach and the *Boolean valued models* approach. In the countable transitive models approach, we force over countable transitive models that live in some larger ambient ${\rm ZFC}$ universe which has all the required generic filters. In the Boolean valued models approach, we find a definable, over $V$, class model of ${\rm ZFC}$ into which our universe $V$ elementary embeds and for which we have a generic filter in $V$ so that we can form its generic extension. Thus, we have classes in our universe which look like a model of ${\rm ZFC}$ and its forcing extension, and moreover this model behaves essentially like $V$ because $V$ elementarily embeds into it. In order to define these models, we pass from a fixed forcing $\mathbb P$ to its Boolean completion $\mathbb B$ (a unique up to isomorphism compelte Boolean algebra of which $\mathbb P$ is a dense subset). With $\mathbb B$, we can build the Boolean valued model $V^{\mathbb B}$ in the language with $\in$ and the predicate $\check V$ for the ground model (defined by $[[\tau\in\check V]]=\bigvee_{x\in V}[[\tau=x]]$). Let $U$ be any ultrafilter on $\mathbb B$ (no genericity is required). Let $V^{\mathbb B}/U$ consist of all $[\tau]_U$ with $\tau\in V^{\mathbb B}$ and $\check V_U$ consist of all $[\tau]_U$ with $[[\tau\in \check V]]\in U$. Then it will be the case that $\check V_U[[\dot G]_U]=V^{\mathbb B}/U$ and there is an elementary embedding $i:V\to \check V_U$, so that we can use $\check V_U$ and $V^{\mathbb B}/U$ as surrogates for $V$ and $V[G]$. For class forcing over models of ${\rm GBC}$, we are forced to adapt the countable transitive models approach because class partial orders don’t need to have Boolean completions (sometimes not even for set-sized suprema). To be more precise, $\mathbb M=(M,\in,\mathcal C)$ of second-order set theory is a countable transitive model if $M$ is countable and transitive, and $\mathcal C$ is a countable collection of subsets of $M$. All results below are about countable transitive models of some second-order set theory. In the general set-up for class forcing, the transitivity requirement can be relaxed to allow for countable nonstandard models, but it has to be carefully checked (by someone) which of the results below transfer to this more general context.

**Forcing Theorem**

Suppose $\mathbb P$ is a notion of forcing. The *Forcing Theorem* for $\mathbb P$ has two parts. The *Definability Lemma* states that for a fixed formula $\varphi(\vec x)$, the set of all $(p,\vec\tau)$ with $p\in\mathbb P$ and $\mathbb P$-names $\vec\tau$ such that $p\Vdash\varphi(\vec\tau)$ is definable. The *Truth Lemma* states that if a forcing extension $V[G]$ by $\mathbb P$ satisfies $\varphi(\vec\tau)$, then there is some condition $p\in G$ with $p\Vdash\varphi(\vec\tau)$. The Forcing Theorem is the most basic fact about set forcing and it can fail for class forcing. Since, it is shown in [2] that the full Forcing Theorem follows from the Definability Lemma for atomic formulas, the failure of the Forcing Theorem for class forcing is already in the definability of atomic formulas. There are two ways to approach this problem. The Forcing Theorem holds for all pretame forcing notions (see [1] or [3]), and so restricting to this class eliminates the worry that the Forcing Theorem fails. It should be noted that there are non-pretame forcing notions for which the Forcing Theorem holds (for instance ${\rm Coll}(\omega,{\rm ORD})$, see [1]). We can also eliminate all such problems by moving to a stronger base theory, for example, ${\rm KM}$. Over ${\rm KM}$ and in fact already over the much weaker theory ${\rm GBC}+{\rm ETR}$ (${\rm ETR}$ is the principle of transfinite recursion over well-founded class relations, which states that every such first-order definable recursion has a solution, see [4] for more details), every class forcing satisfies the Forcing Theorem. The reason is that to prove the Definability Lemma for atomic formulas we need to perform a recursion over a well-founded class relation.

**Boolean completions**

Every separative set partial order $\mathbb P$ is a dense subset of its regular open algebra $\mathbb B$ which is a complete Boolean algebra. This algebra is unique up to isomorphism in the sense that if $\mathbb P$ is a dense subset of any other complete Boolean algebra $\bar {\mathbb B}$, then there is an isomorphism between $\mathbb B$ and $\bar {\mathbb B}$ fixing $\mathbb P$. A class Boolean algebra that has a class-sized antichain can never be complete [3]. So in the context of class forcing the most we can ask for is that every (separative) class partial order is a dense subset of a set-complete Boolean algebra. Even this fails [2]. There are separative class partial orders that don’t have set-complete Boolean completions, and if such a completion does exist it need not be unique [2]. If the Forcing Theorem holds for a forcing notion $\mathbb P$, then $\mathbb P$ has a set-complete Boolean completion [2]. So every pretame notion of forcing has a set-complete Boolean completion. Again, this difficulty can also be eliminated by moving to a stronger theory such as ${\rm KM}$. In models of ${\rm KM}$, every (separative) class partial order $\mathbb P$ is a dense subset of a set-complete Boolean algebra and the regular open algebra of $\mathbb P$ is a definable hyperclass. So we have at least some access to the full Boolean completion of $\mathbb P$, which means that in principle we can attempt the Boolean valued model construction from set forcing.

**Dense embeddings**

If $\mathbb P$ and $\mathbb Q$ are set partial orders such that $\mathbb P$ densely embeds into $\mathbb Q$, then $\mathbb P$ and $\mathbb Q$ have the same forcing extensions. This can fail for class forcing, and the property holding is precisely equivalent to pretameness [3]. As an example of the failure of this property consider again the partial order ${\rm Coll}(\omega,{\rm ORD})$ and the variant ${\rm Coll}_*(\omega,{\rm ORD})$ whose conditions are functions $p:n\to{\rm ORD}$ for some $n\in\omega$. Clearly ${\rm Coll}_*(\omega,{\rm ORD})$ densely embeds into ${\rm Coll}(\omega,{\rm ORD})$, but with a little bit of work it can be shown that ${\rm Coll}(\omega,{\rm ORD})$ adds sets, while ${\rm Coll}_*(\omega,{\rm ORD})$ does not [2].

**Fullness**

Suppose $\mathbb P$ is a set partial order. If $p\in\mathbb P$ and $p\Vdash \exists x\,\varphi(x)$, then there is a $\mathbb P$-name $\tau$ such that $p\Vdash\varphi(\tau)$. This property is called *fullness*. For class notions of forcing, fullness is equivalent to ${\rm ORD}$-cc.

**Nice names**

If $\mathbb P$ is a set forcing, then every subset of ordinals (say of $\alpha$) in a forcing extension has a *nice name*, meaning a $\mathbb P$-name of the form $\bigcup_{\gamma<\alpha}\{\check\gamma\}\times A_\gamma$, where the $A_\gamma$ are antichains of $\mathbb P$. Every forcing extension by ${\rm Coll}(\omega,{\rm ORD})$ has a subset of $\omega$ for which there is no nice name [3]. Pretameness is equivalent to the property that every subset of ordinals in the extension has a nice name. ${\rm ORD}$-cc is equivalent to the property that for every $\mathbb P$-name $\sigma$ such that $1\Vdash\sigma\subseteq\check\alpha$ for some ordinal $\alpha$, there is a nice name $\tau$ such that $1 \Vdash\sigma=\tau$ [3].

**Separation**

We already know that class forcing need not preserve ${\rm GBC}$. Replacement clearly fails in any forcing extension by ${\rm Coll}_*(\omega,{\rm ORD})$. It is a bit trickier to see that Separation fails as well. Let $F:\omega\to{\rm ORD}$ be the surjection added by ${\rm Coll}_*(\omega,{\rm ORD})$. The set $\{n\in\omega\mid F(n)\text{ is odd}\}$ is not in the extension [5]. The failure of this instance of Separation uses a class parameter, namely $F$. It is also true that there is a cardinal and cofinality preserving partial order $\mathbb P$ (satisfying the Forcing Theorem) all of whose extensions have a failure of Separation that does not use class parameters [5].

[Bibtex]

```
@book {friedman:classforcing,
AUTHOR = {Friedman, Sy D.},
TITLE = {Fine structure and class forcing},
SERIES = {de Gruyter Series in Logic and its Applications},
VOLUME = {3},
PUBLISHER = {Walter de Gruyter \& Co., Berlin},
YEAR = {2000},
PAGES = {x+221},
ISBN = {3-11-016777-8},
MRCLASS = {03-02 (03E15 03E35 03E45 03E55)},
MRNUMBER = {1780138},
MRREVIEWER = {A. Kanamori},
DOI = {10.1515/9783110809114},
URL = {http://dx.doi.org/10.1515/9783110809114},
}
```

[Bibtex]

```
@article {PeterHolyRegulaKrapfPhilippLuckeAnaNjegomirPhilippSchlicht:classforcing1,
AUTHOR = {Peter Holy and Regula Krapf and Philipp L\"{u}cke and Ana Njegomir and Philipp Schlicht},
TITLE = {Class Forcing, the Forcing Theorem and Boolean Completions},
NOTE ={To appear in the Journal of Symbolic Logic}
}
```

[Bibtex]

```
@article {PeterHolyRegulaKrapfPhilippSchlicht:classforcing2,
AUTHOR = {Peter Holy and Regula Krapf and Philipp Schlicht},
TITLE = {Characterizations of Pretameness and the {O}rd-cc},
NOTE ={Preprint}
}
```

[Bibtex]

```
@INCOLLECTION{GitmanHamkins:OpenDeterminacyForClassGames,
author = {Victoria Gitman and Joel David Hamkins},
title = {Open determinacy for class games},
booktitle = {Foundations of Mathematics, Logic at Harvard, Essays in Honor of Hugh Woodin's 60th Birthday},
publisher = {American Mathematical Society},
year = {(expected) 2016},
editor = {Andr\'es E. Caicedo and James Cummings and Peter Koellner and Paul Larson},
volume = {},
number = {},
series = {Contemporary Mathematics},
type = {},
chapter = {},
pages = {},
address = {},
edition = {},
month = {},
note = {Newton Institute preprint ni15064},
url = {http://jdh.hamkins.org/open-determinacy-for-class-games},
eprint = {1509.01099},
archivePrefix = {arXiv},
primaryClass = {math.LO},
abstract = {},
keywords = {},
pdf= {http://boolesrings.org/victoriagitman/files/2016/09/Proper-class-games.pdf},
}
```

[Bibtex]

```
@article {PeterHolyRegulaKrapfPhilippSchlicht:classforcing3,
AUTHOR = {Peter Holy and Regula Krapf and Philipp Schlicht},
TITLE = {Separation in Class Forcing Extensions},
NOTE ={Preprint}
}
```

Thanks for this Vika! Fantastically useful post. Two quick remarks:

1. It’s good that when talking about the countable transitive model approach, you specify that the ctm should not just be a ctm for ZFC, but should also be a ctm elementarily equivalent to V. This is especially so if you want to prove facts about your ctm and then export them back to V (e.g. with a generic embedding), rather than just establish a relative consistency proof. This often gets ignored. (Shameless plug: I discuss it a little in a soon-to-be-submitted paper).

2. It’s super-cool that definability of the forcing relation for class forcings is related to the existence of classes (in your case ETR). I wonder how this goes for other kinds of extensions (e.g. sharps)? Interestingly (by some unpublished results of Stanley), satisfaction in *arbitrary* outer models becomes first-order definable if you have certain other slightly-greater-than-first-order conditions on V (from memory: I think the class of Ramsey cardinals has to be definably regular in Hyp(V)). Also, the satisfaction relation for arbitrary outer models is definable using a bit of impredicative comprehension (we’re finalising how much now—second shameless plug: These issues are discussed in a soon-to-be-submitted co-authored paper with myself, Carolin Antos, and Sy Friedman).

Great to hear from you, Neil!

I actually only specified that the ground model of the Boolean valued model should be elementarily equivalent to $V$. Can you say more about how we can get a countable transitive model that is elementarily equivalent to $V$ and why this is important (you mentioned something about generic embeddings)? The papers you mention look super interesting. Do you mind adding links to PDFs if you already have preprints?

Thanks for your replies!

“I actually only specified that the ground model of the Boolean valued model should be elementarily equivalent to V”

That is a good point: Dunno how I missed that (must have been tired and/or rushed)!

“Can you say more about how we can get a countable transitive model that is elementarily equivalent to V”

Obviously V can’t tell that such a ctm provides its own truth definition (by Tarski). Two options:

1. Use a truth predicate, add the Tarski axioms, and permit the use of a truth predicate in the Comprehension and Replacement axioms. Prove reflection, reflect on formula “x is a Godel-code for some phi and Tr(x)”. Then the structure can see a ctm elementarily equivalent to for ZFC-formulas by usual Skolemisation and Collapse. (Thanks to Sam Roberts for mentioning use of truth predicates for this).

2. Extend ZFC with a constant M and the following axioms:

(i) M is countable and transitive.

(ii) \phi \phi^(M) [by Tarski, this has to be a scheme]

This is actually a conservative extension of ZFC.

“and why this is important (you mentioned something about generic embeddings)?”

It depends what you want out of forcing. If you just want your relative consistency proof, then all you need is a ctm for (a big enough finite fragment of) ZFC. But maybe you want to prove some facts about V that go well beyond its ZFC-satisfaction. Maybe you want to do this by combinatorially bolting sets together in the extension. Say you had good reason to believe in the existence of an ideal required to facilitate a generic embedding (as I understand it, we can perfectly well have this in V even if we believe there are no generics for V). But moving to a ctm for ZFC doesn’t guarantee that I can do this construction (it might not have the ideal), or even if it does, that some consequences determined in relation to other facts in V hold in the ctm (our ctm might radically differ to V with respect to other independent facts!). We want a nice, uniform way of getting the most accurate picture possible of extensions *of V*, not a model something-a-bit-like-V.

Of course, technically speaking you could just move to a ctm of (a big enough finite fragment of) ZFC + “Exists an ideal of the required kind” + “Other truths of V”. This isn’t a technical point about the metamathematics of forcing, rather I’m making a point about *philosophical* importance. If you want to mimic extensions *of V*, you need something that looks very much like V but has the generics, not something that looks a little like V.

“Do you mind adding links to PDFs if you already have preprints?”

I’m actually just redrafting the two papers now (as well as making a new website) and so will add a link in the next couple of weeks to this comment thread.

I can’t edit my comment:

Under 2. (ii) it should read \phi \leftrightarrow \phi^M (for some reason, my object-language “iff” got removed on posting).

All very interesting! Thanks Neil and I look forward to reading your papers.

Hey Vika,

So, it took a bit longer than expected to get this ship-shape, but I’m basically there. You can find the ctms paper here:

https://www.academia.edu/31683676/Small_but_Mighty_A_defence_of_the_countable_transitive_model_strategy

and the coding of extensions paper here:

https://www.academia.edu/31683677/Universism_and_Extensions_of_V

There will probably be a few tweaks to be made, but its getting there. The former is submitted, and the latter will be soon!

Best,

Neil