# Substitutional quantification in set theory

Is there a unary formula $$\phi$$ in the language of set theory with the following properties:

(i) $$ZFC \vdash (\exists x)\phi(x)$$

(ii) for each unary formula $$\psi$$ in the language of set theory for which $$ZFC \vdash (\exists! x)\psi(x)$$, we have $$ZFC \vdash (\forall x)(\psi(x) \rightarrow \neg \phi(x))$$

No, such a formula does not exist. The reason is that in $$L$$, the constructible universe, there is a definable well-ordering $$<_L$$ of the universe. Hence, for any formula $$\phi$$ such that $$L\models\exists x\,\phi(x)$$, there is a formula $$\psi_\phi$$ such that $$L\models\exists!x\,\psi_\phi(x)$$ and $$L\models\forall x\,(\psi_\phi(x)\to\phi(x))$$, namely, $$\psi_\phi(x)$$ states that $$x$$ is the $$<_L$$-first witness to $$\phi$$.
Replacing your theory with $$\mathsf{ZFC}+V\ne L$$ does not help either, as we can always use class forcing to make $$V=HOD$$, the class of hereditarily ordinal definable elements, in which case we again have a definable well-ordering of the universe.
On the other hand, it is consistent that a formula as you suggest exists. Not provably, of course, as just indicated, but that some model $$M$$ satisfies the versions of (i) and (ii) in your post with each "$$\mathsf{ZFC}\vdash$$" replaced with "$$M\models$$". Namely, let $$g$$ be a real Cohen generic over $$L$$, and consider $$M=L[g]$$ and $$\phi(x)$$ the statement that $$x$$ is Cohen-generic over $$L$$.
• @AsafKaragila Which satisfy $V=HOD$. Aug 19, 2020 at 17:57