Set forcing over transitive models of NBG

What is known about set forcing over (transitive) models of NBG?

More specifically: Given some set-sized complete Boolean algebra $\mathbb P$ (or simply a poset) it does make sense to introduce proper class $\mathbb P$-names and thinking through the details it seems we still get the full forcing theorem if we allow class $\mathbb P$-names as predicates, defining, for a given class $\mathbb P$-name $C$ $$[\![ \tau \in C ]\!]_{\mathbb P} = \sum_{\mathbb P} \{ [\![\tau = \rho]\!]_{\mathbb P} \mid \rho\in C \}.$$ But what about a forcing theorem for the associated 2nd order language?

• I find it very likely that someone else has asked this, or a very similar question, before. But in my (admittedly short) search for duplicates, the only related question I found was this. – Stefan Mesken Jan 9 '18 at 13:43

Set forcing works over models of ${\rm NBG}$. Suppose ${\mathbb P}$ is a set partial order. Set $\mathbb P$-names are defined as usual. A class $\mathbb P$-name is defined to be a collection of pairs $(\tau,p)$ where $\tau$ is a set $\mathbb P$-name and $p\in\mathbb P$. All the usual properties of the set forcing construction continue to hold in this case. The forcing extension is again a model of ${\rm NBG}$. The forcing theorem holds, namely for a fixed first-order formula $\varphi(x,\Gamma)$ with a fixed class $\mathbb P$-name parameter $\Gamma$, the collection of all pairs $(p, \tau)$ such that $p\Vdash \varphi(\tau,\Gamma)$ is a class. The class is given by the usual first-order recursion to define the forcing relation. It follows from this that for a fixed second-order formula $\varphi(x,X)$ the collection of all triples $(p,\tau,\Gamma)$ such that $p\Vdash\varphi(\tau,\Gamma)$ is definable (complexity of the definition of course depends on the complexity of $\varphi$). Indeed, all the results mentioned above extend to tame class partial orders, a technical property of class forcing isolated by Sy Friedman.

These properties however do not hold of all class partial orders in a model of ${\rm NBG}$. There are class partial orders whose forcing extensions fail to satisfy ${\rm NBG}$ and for which the forcing theorem fails to hold.

A very general account of class forcing (the theorems there of course apply to set forcing) over models of ${\rm NBG}$ can be found in Characterizations of pretameness and the ORD-cc. The weakest theory required for the forcing theorem to hold for all class partial orders is ${\rm NBG}$ together with the principle ${\rm ETR_{\rm ORD}}$. The principle ${\rm ETR_{\rm ORD}}$ states that every first-order recursion of length ${\rm ORD}$ (where stages of the recursion are allowed to be classes) has a solution. This is shown in The exact strength of the class forcing theorem.

Note: Joel David Hamkins just pointed out to me in a discussion that we may not have mixed class names even for set partial orders in ${\rm NBG}$. So it might be the case that a condition $p\Vdash\exists X\varphi(X)$, but there is no class $\mathbb P$-name $\Gamma$ such that $p\Vdash\varphi(\Gamma)$.

• Thank you, Victoria. That's precisely what I was looking for. – Stefan Mesken Jan 9 '18 at 20:40
• Nice answer. I believe that the mixing lemma for class names for set forcing will be equivalent to the <Ord-CC class collection principle (also known as class choice). Indeed, I think we will get $\kappa$-CC from class mixing for the forcing which is a $\kappa$-sized lottery sum of trivial forcing. – Joel David Hamkins Jan 9 '18 at 21:10
• Those references are fascinating, thanks – Not Mike Jan 9 '18 at 23:56

Why are you trying to define $\mathbb{P}$-names for classes? The details of the forcing relation and associated theorems deal explicitly with sets.

The class-extension axiom requires an explicit formula whose quantifiers are restricted to sets. So defining the notion of a $\mathbb{P}$-name for such an object seems unhelpful.

Edit: this was suppose to be a comment..

Edit: Removed random scratch.

• "Why are you trying to define $\mathbb P$-names for classes?" Because I'd like to use them, if possible. "The class-extension axiom requires an explicit formula which is not allowed to quantify over arbitrary classes." Fair enough. What about MK then? (And yes, there are still issues regarding the class of all class names... but it seems like we can deal with that like we do in ZFC with classes, since the relevant $2$-classes are definable.) – Stefan Mesken Jan 9 '18 at 16:42
• @StefanMesken, I feel like you might run into trouble as soon as "Limitation of size" enters the picture. Why not just use NBK and the extension axiom to define for each formula $\varphi$ the class $\{\tau[G]: (\exists p \in G)(p \Vdash \varphi(\tau)\}$? – Not Mike Jan 9 '18 at 17:08
• That's precisely what I've been doing so far. The motivation behind my question is that I was hoping there might be a -- for lack of a better phrase -- more uniform approach dealing with classes in forcing extensions that I just haven't heard of, yet. It's, of course, entirely possible that this approach is doomed to fail. – Stefan Mesken Jan 9 '18 at 17:13