The existence of definable subsets of finite sets in NBG

Question

This question is motivated by my preceding MO-question on (in)consistency of NBG theory of classes.

Let $\varphi(x,Y,C)$ be a formula of NBG with free parameters $x,Y,C$ and all quantifiers running over sets. Godel's Class Existence Theorem ensures that for every classes $Y,C$ the class $\{x:\varphi(x,Y,C)\}$ does exist. On the other hand, the existence of the class $\{x:\exists Y\;\varphi(x,Y,C)\}$ cannot be proved in NBG, see the answer of @AliEnayat to this MO-question.

Question. Can on prove that in NBG for every finite set $F$ and every class $C$ the set $\{x\in F:\exists Y\;\varphi(x,Y,C)\}$ exists?

Answer 1

The answer is in the negative. Let $\mathcal{M}$ be an $\omega$-nonstandard model of ZF, and $\mathfrak{X}$ be the collection of parametrically definable subsets of $\mathcal{M}$. Let $I$ be the cut defined in my answer to the other MO question. Note that by Tarski's undefinability of truth theorem, in the model $(\mathcal{M},\mathfrak{X})$ of NBG, the cut $I$ exactly corresponds to the collection of standard natural numbers. Also note that the definition of $I$ is $\Sigma^1_1$.

Let $c$ be a nonstandard natural number of $\mathcal{M}$, and let $F$ be the finite set (in the sense of $\mathcal{M}$) of the predecessors of $c$. Then the collection of members of $F$ that belong to $I$ has a $\Sigma^1_1$-definition, but it does not exist in the model (since it is a subset of natural numbers of the model that is bounded above but has no maximum).

In the above, if one wishes to do away with the nonstandard parameter $c$ in the construction of the counterexample, one can choose $\mathcal{M}$ to satisfy $\lnot \mathrm{Con(ZF)}$, and use "the shortest proof of the inconsistency of $\mathrm{Con(ZF)}$" instead of $c$.