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.

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.

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 defined by analogy with number/set quantifiers:

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

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.

Let $A, B, C..X, Y$ range over potentially proper classes in NBG set theory 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 defined by analogy with number/set quantifiers:

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

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 defined by analogy with number/set quantifiers:

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