Boolean-valued class forcing
C. Antos, S.-D. Friedman, and V. Gitman, “Boolean-valued class forcing,” Fund. Math., vol. 255, no. 3, pp. 231–254, 2021.
There are two standard approaches to carrying out the forcing construction over a model of ${\rm ZFC}$ set theory: with partial orders or with complete Boolean algebras. The two approaches yield the same forcing extensions because every partial order densely embeds into a complete Boolean algebra, and when a partial order densely embeds into another partial order, the two have the same forcing extensions. Although the partial order construction can be viewed as more straightforward, the complete Boolean algebras approach offers some advantages. For instance, there are theorems about forcing which have no known proofs without the use of Boolean algebras. One such fundamental result is the Intermediate Model Theorem, which states that if a universe $V\models{\rm ZFC}$ and $W\models{\rm ZFC}$ is an intermediate model between $V$ and one of its set-forcing extensions, then $W$ is itself a forcing extension of $V$. The theorem makes a fundamental use of the Axiom of Choice, but a weaker version of it still holds for models of ${\rm ZF}$. If $V\models{\rm ZF}$ and $V[a]\models{\rm ZF}$, with $a\subseteq V$, is an intermediate model between $V$ and one of its set-forcing extensions, then $V[a]$ is itself a set-forcing extension of $V$. Grigorieff in [1] attributes the Intermediate Model Theorem to Solovay.
The standard Boolean algebras approach is not available in the context of class forcing because most class partial orders cannot be densely embedded into a sufficiently complete class Boolean algebra. Set forcing uses complete Boolean algebras, those which have suprema for all their subsets, because completeness is required for assigning Boolean values to formulas in the forcing language. With a class Boolean algebra, which has suprema for all its subsets, we can still define the Boolean values of atomic formulas, but the definition of Boolean values for existential formulas needs to take suprema of subclasses, meaning that we must require a Boolean algebra to have those in order to be able to construct the Boolean-valued model. However, as shown in [2], a class Boolean algebra with a proper class antichain can never have this level of completeness. Thus, only ${\rm ORD}$-cc Boolean algebras (having set-sized antichains) can potentially have suprema for all their subclasses. Indeed, it is shown in [2] that every ${\rm ORD}$-cc partial order densely embeds into a complete Boolean algebra.
In this article we nevertheless show that the Boolean algebras approach to class forcing can be carried out in sufficiently strong second-order set theories, for example, the theory Kelley-Morse plus the Choice Scheme, using hyperclass Boolean completions. We apply the Boolean algebras approach to show that the ${\rm ZF}$-analogue of the Intermediate Model Theorem holds for models of Kelley-Morse plus the Choice Scheme.
Let us call an extension $\mathscr W$ of a model $\mathscr V$ of second-order set theory simple if it is generated by the classes of $\mathscr V$ together with a single new class. In particular, every forcing extension of $\mathscr V$ is simple. We show that every simple intermediate model between a model of ${\rm KM}+{\rm CC}$ and one of its class forcing extensions is itself a forcing extension, so that the Intermediate Model Theorem holds for simple extensions. We also show that an intermediate model between a model of ${\rm KM}+{\rm CC}$ and one of its class forcing extensions need not be simple, and thus the Intermediate Model Theorem can fail. For models of ${\rm KM}$, the Intermediate Model Theorem can fail even where the forcing has the ${\rm ORD}$-cc because a model of ${\rm KM}$ and its forcing extension by ${\rm ORD}$-cc forcing can have non-simple intermediate models. We don't know whether this can happen for models of ${\rm KM}+{\rm CC}$. Finally, we show that if an intermediate model $\mathscr W$ between a model $\mathscr V\models{\rm KM}+{\rm CC}$ and its forcing extension $\mathscr V[G]$ has a definable global well-ordering of classes, and we have additionally that $\mathscr W$ is definable in $\mathscr [G]$, then $\mathscr W$ must be a simple extension of $\mathscr V$.
References
- S. Grigorieff, “Intermediate submodels and generic extensions in set theory,” Ann. Math. (2), vol. 101, pp. 447–490, 1975.
- 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.