In NBG (ZFC + classes) if $P$ nonempty predicate of classes must $P$ have definable solution?

Question

Let $A, B, C..X, Y$ range over potentially proper classes in NBG set theory (or adding class quantification to ZFC in obvious way) and $x,y,z$ range over sets.

Since I don't know the proper symbols for formula classes that have $n$ proper class quantifiers I'll just continue the convention of add 1 to the upper subscript ($\Sigma^0_n/\Sigma^1_n$) as we move to quantifying over a higher type of object.

• $P(C)$ is a $\Sigma^2_0=\Pi^1_0$ class predicate if $P(C) \iff \phi(C)$ where $\phi(C)$ only contains set quantifiers.
• $P(C)$ is a $\Sigma^2_{n+1}$ ($\Pi^2_{n+1}$) class predicate if $P(C)$ has the form $(\exists X) Q(C,X)$ ($(\forall X) Q(C,X)$ ) where $Q$ is a $\Sigma^2_{n}$ ($\Pi^2_{n}$) class predicate.

Suppose $P(C)$ is a non-empty $\Sigma^2_0$ class predicate, i.e., $P(C)$ is equivalent to a formula quantifying only over sets. Must there be a definable class $B$ satisfying $P(B)$ (where definable means definable via quantification over sets no proper classes...so same thing as in ZFC)? What if $P(C)$ is instead $\Sigma^2_n/\Pi^2_n$?

I'm tempted to think the answer is yes (at least for $\Sigma^2_0$). However, it seems to me that you can think of this as asking whether there is a (full height of $V$) path through a certain tree of classes and what is going on seems very similar to the question of whether every nonempty arithmetic tree has a $\Delta^1_1$ path where the answer is no. Indeed there is a $\Pi^0_2$ class with no $\Delta^1_1$ path and as that is exactly where things started to fail for me with the class question it seems the evidence says no even in that case.

Also I'm probably just failing to think of something simple since my set theory is rusty.

Remark on Intended Question

Turns out the question I was interested in was for MK set theory not NBG (so one can comprehend with formulas involving class quantifiers) but I'd forgotten they were different. Luckily the answer below answered that as well.

Answer 1

Your superscripts are all off by one with respect to the usual notation. That is, $\Sigma^0_n$ in the language of set theory means we have first-order quantifiers only, that is, over sets, whereas $\Sigma^1_n$ means we have $n$ alternations of second-order quantifiers (over classes).

If one is speaking of first-order formulas and set objects only, then the property in a model of set theory that every definable class $\{x\mid\varphi(x)\}$ has a definable element is equivalent to $V=\text{HOD}$, because the class of non-OD sets is certainly definable, but can have no definable element, and so it must be empty if the property is to hold; conversely, if $V=\text{HOD}$ holds, then there is a definable well-ordering of the universe, and so the definable class has a least member with respect to that well-order, and this object will be definable.

So the models of set theory in which every definable class has a definable element are exactly the models of V=HOD.

But you seem to be interested not in defining classes of sets, but rather in properties of classes $C$. That is, if $\varphi$ is a property of a class $C$ and there is a class $C$ such that $\varphi(C)$, then is there a definable class $C$ for which $\varphi(C)$?

Here, the answer is: not necessarily. For example, consider a model of NGBC that has a truth-predicate $T$ for first-order truth. For example, any model of Kelley-Morse set theory is like that, but considerably less than KM suffices. Now, the assertion that "$T$ is a truth predicate" is a first-order expressible property of $T$, since one need only say that $T$ obeys the Tarskian recursion. But there can be no definable class $T$ that is a truth predicate, because of Tarski's theorem on the non-definability of truth.

Meanwhile, there are models of NGB set theory that are pointwise definable, meaning that every set and class is definable without parameters. For example, see my paper:

• Hamkins, Joel David; Linetsky, David; Reitz, Jonas, Pointwise definable models of set theory, J. Symb. Log. 78, No. 1, 139-156 (2013), http://dx.doi.org/10.2178/jsl.7801090. (ZBL1270.03101).

In such a model, if there is a class $C$ with property $\varphi(C)$, then $C$ is already definable, because all classes in such a model are definable.

So the answer is that it is sometimes true, and sometimes not true, depending on your model of NGB.