Forcing to add proper classes to a model of ${\rm GBC}$: The technicalities

In the previous post Forcing to add proper classes to a model of ${\rm GBC}$: An introduction, I made several sweeping assertions that will now be held up to public scrutiny.

Recall the set-up: $\langle M,\mathfrak M,\in\rangle$ is a model of ${\rm GBc}$ (or ${\rm GBC}$), $\mathbb P\in\mathfrak M$ is a class partial order that is strategically $\lt\kappa$-closed for every cardinal $\kappa$ in $M$. The forcing language consists of $\mathbb P$-class name predicates, constants for elements of $M$ and the $\in$ relation. Now we aim to prove that the resulting forcing relation $\Vdash$ satisfies the three key forcing lemmas, and use them to conclude that $\langle M,\mathfrak M[G],\in\rangle $ is a model of ${\rm GBc}$ (or ${\rm GBC}$).

Following Shoenfield [1], we will first argue that the three lemmas hold for the auxiliary forcing relation $\Vdash^*$, which we define below. We will then argue that $p\Vdash\varphi$ if and only if $p\Vdash^*\neg\neg\varphi$, from which the three lemmas for $\Vdash$ will follow. The definition of $\Vdash^*$ is a drastically simplified version of Shoenfield's because there is no recursion involved in $\mathbb P$-class names.

We define the relation $\Vdash^*$ as follows:

  1. $p\Vdash^* a\in \dot A$ if and only if $\exists q\geq p$ with $\langle a,q\rangle\in \dot A$,
  2. $p\Vdash^*\neg\varphi$ if and only if $\forall q\leq p$, it is not true that $q\Vdash^*\varphi$,
  3. $p\Vdash^*\varphi\vee\psi$ if and only if $p\Vdash^*\varphi$ or $p\Vdash^*\psi$,
  4. $p\Vdash^*\exists x\varphi(x)$ if and only if $\exists a\in M\,p\Vdash^*\varphi(a)$.

The Definability Lemma and the Extension Lemma follow immediately from the definition. So let's prove the Truth Lemma.

Truth Lemma: Suppose that $\varphi$ is a sentence of the forcing language mentioning only $\mathbb P$-class names $\dot A_1,\ldots,\dot A_n$. If $G\subseteq\mathbb P$ is $\mathfrak M$-generic, then $\langle M,(\dot A_1)_G,\ldots,(\dot A_n)_G\rangle\models\varphi$ if and only if there is $p\in G$ such that $p\Vdash\varphi$.

Proof: The proof is by induction on complexity of formulas. First the atomic case. Suppose that $\langle M,\dot A_G,\in\rangle\models a\in A_G$. Then there is $p\in G$ such that $\langle a,p\rangle\in\dot A$ and so $p\Vdash^*a\in\dot A$. Now suppose that there is $p\in G$ such that $p\Vdash^*a\in\dot A$. So, by definition, there is $q\geq p$ with $\langle a,q\rangle\in\dot A$. But then $q\in G$ and hence $\langle M,\dot A_G,\in\rangle\models a\in \dot A_G$. Next, the negation case. Observe that for a fixed sentence $\varphi$ of the forcing language, the class $D=\{p\in\mathbb P\mid p\Vdash^*\varphi\text{ or }p\Vdash^*\neg\varphi\}$ is dense because if it is not true that $p\Vdash^*\neg\varphi$, then, by definition, there is $q\leq p$ such that $q\Vdash^*\varphi$. Suppose that $\langle M,(\dot A_1)_G,\ldots,(\dot A_n)_G\rangle\models\neg\varphi$. Then, by inductive assumption, there cannot be any $p\in G$ such that $p\Vdash^*\varphi$, and so, by our observation, there must be $p\in G$ such that $p\Vdash^*\neg\varphi$. Now suppose that $p\in G$ such that $p\Vdash^*\neg\varphi$. There cannot be $q\in G$ such that $q\Vdash^* \varphi$ because, if this was the case, since $p$ and $q$ are compatible, there would be $r\leq p$ such that $r\Vdash^* \varphi$. So, by inductive assumption, $\langle M,\dot A_G,\in\rangle\models\models\neg\varphi$. The cases of disjunction and existential quantifier are nearly immediate from the definition. $\square$

Now as promised, we confirm that $p\Vdash\varphi$ if and only if $p\Vdash^*\neg\neg\varphi$. Recall that we defined $p\Vdash\varphi$ (mentioning $\mathbb P$-class names $\dot A_1,\ldots,\dot A_n$) to mean that whenever $G$ is $\mathfrak M$-generic and $p\in G$, then $\langle M,(\dot A_1)_G,\ldots,(\dot A_n)_G,\in\rangle\models\varphi$.

Translation Lemma: If $p\in\mathbb P$ and $\varphi$ is a sentence in the forcing language, then $p\Vdash\varphi$ if and only if $p\Vdash^*\neg\neg\varphi$.

Proof: Fix a sentence of the forcing language mentioning some class $\mathbb P$-names $\dot A_1,\ldots,\dot A_n$. Suppose that $p\Vdash\varphi$. To show that $p\Vdash^*\neg\neg\varphi$, we must check that no $q\leq p$ is such that $q\Vdash^*\neg\varphi$. But if $q\leq p$ is such that $q\Vdash^*\neg\varphi$ and $G$ is $\mathfrak M$-generic containing $q$, then $\langle M,(\dot A_1)_G,\ldots,(\dot A_n)_G\rangle\models\neg\varphi$ by the Truth Lemma for $\Vdash^*$, which is impossible by the assumption that $p\Vdash\varphi$. Thus, $p\Vdash^*\neg\neg\varphi$. Now suppose that $p\Vdash^*\neg\neg\varphi$. Fix an $\mathfrak M$-generic $G$ with $p\in G$. By the Truth Lemma, we have that $\langle M,(\dot A_1)_G,\ldots,(\dot A_n)_G\rangle\models\neg\neg\varphi$, and so $\langle M,(\dot A_1)_G,\ldots,(\dot A_n)_G\rangle\models\varphi$. $\square$

Everything is now in place to argue that $\langle M,\mathfrak M[G],\in\rangle$ is a model of restricted class comprehension and replacement.

Lemma: The model $\langle M,\mathfrak M[G],\in\rangle$ satisfies restricted class comprehension.

Proof: Fix a formula $\varphi(x)$ with class parameters $A_1,\ldots,A_n\in\mathfrak M[G]$, some set parameters, and only set ranging quantifiers. Let $A=\{a\in M\mid \langle M,\mathfrak M[G],\in\rangle\models\varphi(a)\}$. Clearly, $A=\{a\in M\mid \langle M,A_1,\ldots,A_n,\in\rangle\models\varphi(a)\}$. Fix $\mathbb P$-class names $\dot A_1,\ldots, \dot A_n$ such that $(\dot A_i)_G=A_i$. Consider the $\mathbb P$-class name $\dot A=\{\langle a,p\rangle\mid p\in \mathbb P, p\Vdash\varphi(a)\}$. We will argue that $\dot A_G=A$. Suppose that $a\in A$, then $\langle M,A_1,\ldots,A_n,\in\rangle\models\varphi(a)$, and so there is $p\in G$ such that $p\Vdash\varphi(a)$. It follows that $\langle a,p\rangle\in \dot A$, and so $a\in\dot A_G$. Now suppose that $a\in\dot A_G$. Then there is $p\in G$ such that $\langle a,p\rangle\in \dot A$. It follows that $p\Vdash \varphi(a)$, and so $\langle M,A_1,\ldots,A_n,\in\rangle\models\varphi(a)$, meaning that $a\in A$. $\square$

<

strong>Lemma: The model $\langle M,\mathfrak M[G],\in\rangle$ satisfies replacement.

Proof: Fix a function $F\in \mathfrak M[G]$ and $a\in M$. Suppose to the contrary that $F\upharpoonright a$ is not in $M$. Fix a $\mathbb P$-class name $\dot F$ such that $\dot F_G=F$ and a condition $p\in \mathbb P$ such that $p\Vdash\dot F\upharpoonright a\notin \check M$. Next, fix any enumeration $\langle a_\xi\mid\xi<\kappa\rangle$ of $a$. Using that $\mathbb P$ is strategically $\leq\kappa$-closed, we build a descending sequence of conditions $p_\xi$ for $\xi\leq\kappa$ below $p$ with $p_\xi$ deciding $F(a_\xi)$ and $p_\kappa$ thus deciding $\dot F\upharpoonright a$. But then $p_\kappa\leq p$ and $p_\kappa\Vdash\dot F\upharpoonright a\in \check M$, which is the sought after contradiction. $\square$

So let's force to extend a model $\langle M,\mathfrak M,\in\rangle\models{\rm GBc}$ to a model $\langle M,\mathfrak M[G],\in\rangle\models{\rm GBC}$! Let $\mathbb P\in \mathfrak M$ be the class partial order whose conditions are set functions from an ordinal into $M$ ordered by inclusion. The partial order $\mathbb P$ is clearly $\lt\kappa$-closed for every $\kappa$ and also clearly any $\mathfrak M$-generic $G\subseteq\mathbb P$ is a global well-order! What else can we do with this forcing construction?

  1. Add an ${\rm ORD}$-Souslin tree
  2. Add a Cohen subset to ${\rm ORD}$

Any ideas from the readers?

References

  1. J. R. Shoenfield, “Unramified forcing,” in Axiomatic Set Theory (Proc. Sympos. Pure Math., Vol. XIII, Part I, Univ. California, Los Angeles, Calif., 1967), Providence, R.I.: Amer. Math. Soc., 1971, pp. 357–381.