13
$\begingroup$

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,

Improve this question
$\endgroup$
4
  • $\begingroup$ I once asked a related question: mathoverflow.net/questions/81082/… $\endgroup$
    – Michael Greinecker
    Commented Mar 5, 2013 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
    Commented Mar 5, 2013 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
    Commented Mar 5, 2013 at 17:03
  • $\begingroup$ What you described in your question is known as the existence property. It is known that Heyting arithmetic satisfies this property, and Hamkins' answer shows $\mathsf{ZF}$ does not satisfy it. Andrew Swan proved that $\mathsf{CZF}$ also does not satisfy the existence property, and if my memory serves right, $\mathsf{IZF}$ also does not have this property (maybe due to H. Friedman.) $\endgroup$
    – Hanul Jeon
    Commented Feb 3, 2021 at 15:09

1 Answer 1

Reset to default
13
$\begingroup$

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

Improve this answer
$\endgroup$
6
  • 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
    Commented Mar 5, 2013 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
    Commented Mar 5, 2013 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
    Commented Mar 5, 2013 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$
    – user21349
    Commented Mar 5, 2013 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
    Commented Mar 5, 2013 at 22:12

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .