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


Where can I read about it?




---


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?



Set forcing over transitive models of NBG
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](http://www.math.uni-bonn.de/people/pholy/Pretameness_revised.pdf). 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](http://www.math.uni-bonn.de/people/pholy/Strength.pdf). 


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


