Forcing to add proper classes to a model of ${\rm GBC}$: An introduction

If you are interested in a mathematical universe whose ontology includes both sets and classes, you might consider for its foundation the ${\rm GBC}$ (Gödel-Bernays) axioms.

There are two ways to view models of ${\rm GBC}$. One way is to consider structures $\langle M,\mathfrak M,\in\rangle$ in a two-sorted language with $\langle M,\in\rangle$ being the first-order part and $\mathfrak M\supseteq M$ the classes. But we can also think of such a model as an ordinary first-order structure whose elements are classes, where we distinguish as sets those classes that are elements of other classes. The ${\rm GBC}$ axioms for sets are standard: extensionality, foundation, pairing, infinity, union, and powerset. The ${\rm GBC}$ axioms for classes are:

  1. extensionality,
  2. restricted class comprehension for formulas allowing class parameters but quantifying only over sets,
  3. a replacement axiom stating that the restriction of a class function to a set is a set,
  4. existence of a global well-order.

For easy reference, let's call ${\rm GBc}$, the theory that's identical to ${\rm GBC}$ but in that it has just set choice instead of global choice. A model $M$ of ${\rm ZFC}$ together with its collection of definable classes $\mathfrak M$ is clearly a model of ${\rm GBc}$ but not necessarily a model of ${\rm GBC}$, since it may not have a definable global well-order. So is it possible to extend $\mathfrak M$ to a collection of classes $\mathfrak M^*$ making $\langle M,\mathfrak M^*,\in\rangle$ a model of ${\rm GBC}$? More generally, given a model of ${\rm GBc}$ or ${\rm GBC}$, is there a robust method to add proper classes with interesting properties without adding sets? Yes, by forcing! For instance, one often comes across the assertion in set theoretic literature that it is possible add a global well-order without adding sets because the (class) partial order to do so is $\lt\kappa$-closed for every cardinal $\kappa$. But why in the world is the forcing extension by such a partial order (whatever that might even mean) a model of ${\rm GBC}$? What is the forcing language? Are there names for classes, and if so, what are they? Is the forcing relation definable? Does the Truth Lemma hold? I recently discussed an interpretation of it all with Joel Hamkins, which provides definite (if not fully satisfactory) answers to the above questions.

Here is the set-up. Suppose that $\langle M,\mathfrak M,\in\rangle$ is a model of ${\rm GBc}$. Let $\mathbb P$ be a class partial order in $\mathfrak M$ that is strategically $\lt\kappa$-closed for every cardinal $\kappa$. Define that a $\mathbb P$-class name is any class consisting of pairs $\langle a,p\rangle$ with $a\in M$ and $p\in \mathbb P$. Here are two important examples: $\dot G=\{\langle p,p\rangle\mid p\in\mathbb P\}$ and $\check A=\{\langle a,p\rangle\mid a\in A,p\in\mathbb P\}$, where $A\in \mathfrak M$. The forcing language for $\mathbb P$ consists of:

  1. constants $a$ for every set $a\in M$,
  2. predicates $\dot A$ for every $\mathbb P$-class name $\dot A$,
  3. the $\in$-relation.

As is usual, we define that $G\subseteq\mathbb p$ is $\mathfrak M$-generic if $G$ meets every dense class of $\mathbb P$ in $\mathfrak M$. Let $\mathfrak M[G]$ be the collection of all $\dot A_G$ for a class $\mathbb P$-name $\dot A$. Note that $\dot G_G=G$ and $\check A_G=A$, meaning that $\mathfrak M\subseteq\mathfrak M[G]$ and $G\in\mathfrak M[G]$. Suppose that $p\in\mathbb P$ and $\varphi$ is a sentence of the forcing language mentioning $\mathbb P$-class names $\dot A_1,\ldots,\dot A_n$. We define $p\Vdash \varphi$ to mean that the first-order structure $\langle M,(\dot A_1)_G,\ldots, (\dot A_n)_G\rangle\models\varphi$ whenever $G$ is $\mathfrak M$-generic and $p\in G$. Our first aim is prove the three key lemmas about forcing: Definability Lemma, Extension Lemma, and Truth Lemma.

Definability Lemma: If $\varphi(x_1,\ldots,x_n)$ is a formula in the forcing language with free variables $x_1\ldots,x_n$, then $\{\langle p,a_1,\ldots,a_n\rangle\mid p\Vdash \varphi(a_1,\ldots,a_n)\}$ is in $\mathfrak M$.

Extension Lemma: If $p\Vdash\varphi$ and $q\leq p$, then $q\Vdash\varphi$.

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

The forcing lemmas will allows us to prove that $\langle M,\mathfrak M[G],\in\rangle$ satisfies restricted class comprehension and replacement, making it a model of ${\rm GBc}$ (or ${\rm GBC}$). By this we have fulfilled the goal of using the forcing method to add proper classes without adding sets. But what we failed to achieve is access to full truth about the ${\rm GBC}$ model $\langle M,\mathfrak M[G],\in\rangle$ via the forcing relation. The forcing relation cannot tell us anything about formulas that quantify over classes. Luckily though this is not needed in any applications of such forcing techniques that I know of. In the next post, we dive right into the technicalities.