This question is motivated by my preceding [MO-question](https://mathoverflow.net/q/444393/61536) on (in)consistency of [NBG theory of classes](https://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory).


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](https://mathoverflow.net/a/444549/61536) of @AliEnayat to [this MO-question](https://mathoverflow.net/q/444393/61536).



> 
> **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?
> 
> 
> 



The existence of definable subsets of finite sets in NBG
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](https://mathoverflow.net/questions/444393/a-contradiction-in-the-set-theory-of-von-neumann-bernays-g%C3%B6del/444549?noredirect=1#comment1147821_444549). 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$.


