Hi everyone,
This is a question I have been asking from long, but none of my colleagues could ever answer me:
It is a well-known fact that the axiom of choice (AC) allows one to prove the existence of some set with some property $P$, though we cannot exhibit such a set: for instance, one knows that there exists a well-ordering on $\mathbb{R}$, but cannot define any though.
In formal terms, this means the following: working is the ZFC system, one can find a (first-order) logical property $P(x)$ (with one free variable) such that
$$\vdash (\exists x) (P(x)),$$
yet there is no logical property $Q(x)$ such that
$$\vdash (\exists! x) (P(x) \wedge Q(x))$$
Apparently that is the very phenomenon why many people are dubious about the relevance of AC. Yet I have seen nowhere the statement (and even less the proof) that such a phenomenon would not occur in ZF…
So, is it true that, whenever ZF proves the existence of a set having some property, it is also possible to define some non-ambiguous such set?
Regards,
Best Answer
If ZF is consistent, then the answer is no.
ZF proves that there is an $x$ such that $P(x)$: either $x$ is an $L$-generic Cohen real or there is no $L$-generic such real. (Here, by $L$ I mean the constructible universe of Gödel.)
In a universe with $L$-generic Cohen reals, $P$ holds only of them, but in a universe without any $L$-generic Cohen reals, $P$ holds of everything.
But if ZF is consistent, then it cannot prove that there is a definable such object satisfying $P(x)$, because we may consider the forcing extension $L[c]$ obtained by adding an $L$-generic Cohen real. In such a model $L[c]$, which still satisfies ZF, the predicate $P$ holds only of the $L$-generic Cohen reals, but no such real is definable in $L[c]$ because the forcing is almost homogeneous, and consequently all ordinal definable objects of $L[c]$ are in the ground model $L$.
Since these are also ZFC models, they also serve to establish the claim you had made about ZFC having this phenomenon. Indeed, there can be no (parameter-free) definable well-ordering of the reals in $L[c]$, since in this case there would be a definable $L$-generic Cohen real, namely, the least one to appear in the well ordering. Meanwhile, in $L[c]$ there is a $c$-definable well-ordering of $\mathbb{R}$, of complexity $\Delta^1_2(c)$, just as in $L$ there is a parameter-free $\Delta^1_2$ definable well ordering of $L$.
But actually, I've realized that any example from the ZFC case can be transformed to the ZF case by this procedure. In other words, suppose that $P$ has your property for ZFC. Let $P'(x)$ assert "either $P(x)$ or there are no instances of $P$". So ZF proves the existence of $x$ for which $P'(x)$. But there can be no $Q$ that ZF proves to define such an $x$, since such a $Q$ would also ZFC-provably define an $x$ for which $P(x)$, which we had assumed was not the case.
Indeed, as mentioned by Rodrigo in the comments, any subtheory of ZFC at all proves $\exists x\ P'(x)$, but no such theory can prove that there is a definable such $x$, since we assumed that ZFC itself does not prove that there is a definable $x$ for which $P(x)$.