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

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.

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:

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.

• Yes, they are DELIBERATELY off by 1 from the usual notion because you go from 0 to 1 when you switch from number to set quantifier and here I switched again to proper class quantifier. – Peter Gerdes Jun 2 '17 at 3:23
• Well, deliberate or not, I had meant that your notation $\Sigma^1_n$ and $\Sigma^2_n$ is definitely wrong with respect to established usage for your stated meaning. In the usual notation for second- and higher-order set theory, $\Sigma^2_n$ would be understood to refer to quantification over collections of classes, that is, third order set theory. In various set-theoretic contexts, one sees $\Sigma^m_n$, and this notation is fairly universally agreed upon. For this reason, you may want to edit your question to use the standard notation, since otherwise it is confusing. – Joel David Hamkins Jun 2 '17 at 4:06
• Also I see where much of the confusion in notation/question came from. I was taking NBG to be a two-sorted theory with separate sorts for class and set while you were talking in terms of (as I now convinced is more elegant) a 1 sorted theory. You are right the second question was essentially what I was after (your answer covers the one minor difference). – Peter Gerdes Jun 2 '17 at 4:12
• I agree with you if you are working in a theory where set and class are part of the same sort but one at least CAN present NBG where they are two sorts...kinda ugly but that's what I was presuming and then you are moving one type up..hence the motivation.. But yes, I presumed it was wrong...but I still have no idea if there is any notation that distingushes between possibly proper class quantifiers and set (for you non-proper class) quantifiers). – Peter Gerdes Jun 2 '17 at 4:13
• I usually use NBG as a two-sorted theory, and I'm not sure why you thought I use it as one sorted. But it doesn't really matter, since the usual notation for $\Sigma^0_n$ and $\Sigma^1_n$ doesn't depend on that. The superscript $0$ always means first-order, quantification over sets, and the superscript $1$ always means second-order, quantification over classes, whether or not one organizes it into one sort or two. This parallels the usage in arithmetic, where first-order means quantification over numbers and second-order means quantification over sets of numbers, or equivalently, over reals. – Joel David Hamkins Jun 2 '17 at 4:19