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?


  • $\begingroup$ I once asked a related question: mathoverflow.net/questions/81082/… $\endgroup$ – Michael Greinecker Mar 5 '13 at 12:51
  • $\begingroup$ Maybe we heed help with terminology in headlines. Yesterday there was a question (mathoverflow.net/questions/123482 ) where "non-constructive" meant "proof uses the law of the excluded middle". $\endgroup$ – Gerald Edgar Mar 5 '13 at 13:46
  • $\begingroup$ The term `constructive' is indeed over-loaded, but seems to be completely standard for these different usages. One has constructive logic, where excluded middle is not valid; constructive proofs, an informal concept meaning that the proof does not appeal to pure-existence axioms; and the constructible universe $L$, which is the model of set theory that Goedel had created to prove the relative consistency of ZFC+CH. $\endgroup$ – Joel David Hamkins Mar 5 '13 at 17:03

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)$.

  • 2
    $\begingroup$ The problem with this (bad) understanding of the nonconstructive character of AC arises within logic itself. Suppose that $P$ has the property for ZFC. Let $P^′$ be $\exists x P\rightarrow P$. In this case, $\exists x P^′$ is a theorem from logic which has no definable witness in ZFC. This stuff is analyzed in my paper "On Existence in Set Theory", NDJFL, v. 53, n.4, 2012. $\endgroup$ – Rodrigo Freire Mar 5 '13 at 12:10
  • $\begingroup$ Something interesting to note about your final paragraph is that it only works in classical logic. There are examples in intuitionistic set theory where it does not work. $\endgroup$ – aws Mar 5 '13 at 12:29
  • $\begingroup$ Terrific! I did not expect that the proof would be so simple... I wish I asked it on MO earlier ;-) Thanks again! $\endgroup$ – Rémi Peyre Mar 5 '13 at 14:45
  • $\begingroup$ I wonder whether this is a universal idea or just something specific to ZF(C). Are there, e.g., any examples of interesting, widely studied systems in which the nonconstructive axioms are an infinite axiom schema? In a case like that, the argument given above would fail. $\endgroup$ – Ben Crowell Mar 5 '13 at 20:29
  • 1
    $\begingroup$ Rodrigo, indeed, my example about generic Cohen reals has your form. I have edited the final example also into this same form, since it shows that every subtheory of ZFC also admits the properties. $\endgroup$ – Joel David Hamkins Mar 5 '13 at 22:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.