Constructibility of uniquely defined sets in ZFC.

Question

I was thinking about constructible universe, and I had the following idea.

Suppose we have a predicate $\phi$ defined in a language of set theory. Suppose moreover, that the statement "there exists $X$ such that $\phi(X)$; and for any $X, Y$ if $\phi(X)$ and $\phi(Y)$, then $X=Y$" is provable in ZFC (essentially, that the formula $\phi$ determines a unique set). Then that set $X$ must belong to some level $L_\alpha$ of the constructible hierarchy.

The argument is as follows: since the existence and uniqueness is provable in ZFC, it must be true in the constructible universe, which is a model of ZFC. But since constructible universe is an inner model of ZFC, that particular element of the constructible universe that serves as a witness of the truth of the formula in the constructible universe model of ZFC must also be the unique $X$ in the "whole" ZFC$-$we cannot have a different one, because there is already a set that satisfies $X$ in the constructible hierarchy.

Is this argument sound? It feels solid and completely obvious to me, and vacuous at the same time.

Answer 1

The argument is clearly wrong. $\mathcal P(\omega)$ is definable without parameters, and yet it is not necessarily constructible, as shown by Cohen.

The thing to remember is that the formula $\phi$ is not absolute between models. So $\mathcal P(\omega)$ and $\mathcal P(\omega)^L$ might be different.

In some cases, there are sets whose definition is very robust and unique, but they cannot even exist in $L$. One example of this kind is $0^\#$, which has a parameter free definition, and can be represented as a fairly canonical set of integers. But nevertheless, this set cannot exist in $L$. Other examples would be any real, since you can code it into the continuum pattern below $\aleph_\omega$ (for example), and even much more than that.