The oddities of class forcing

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 (missing reference).

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].

References

  1. S. D. Friedman, Fine structure and class forcing, vol. 3. Walter de Gruyter & Co., Berlin, 2000, p. x+221.
  2. P. Holy, R. Krapf, P. Lücke, A. Njegomir, and P. Schlicht, “Class forcing, the forcing theorem and Boolean completions,” J. Symb. Log., vol. 81, no. 4, pp. 1500–1530, 2016.
  3. P. Holy, R. Krapf, and P. Schlicht, “Characterizations of pretameness and the Ord-cc,” Ann. Pure Appl. Logic, vol. 169, no. 8, pp. 775–802, 2018.
  4. V. Gitman and J. D. Hamkins, “Open determinacy for class games,” in Foundations of mathematics, vol. 690, Amer. Math. Soc., Providence, RI, 2017, pp. 121–143.
  5. P. Holy, R. Krapf, and P. Schlicht, “Sufficient conditions for the forcing theorem, and turning proper classes into sets,” Fund. Math., vol. 246, no. 1, pp. 27–44, 2019.