I think I'm a bit confused about the relationship between some concepts in mathematical logic, namely constructions that require the axiom of choice and "explicit" results.

For example, let's take the existence of well-orderings on $\mathbb{R}$. As we all know after reading this answer by Ori Gurel-Gurevich, this is independent of ZF, so it "requires the axiom of choice." However, the proof of the well-ordering theorem that I (and probably others) have seen using the axiom of choice is nonconstructive: it doesn't produce an explicit well-ordering. By an explicit well-ordering, I simply mean a formal predicate $P(x,y)$ with domain $\mathbb{R}\times\mathbb{R}$ (i. e., a subset of the domain defined by an explicit set-theoretic formula) along with a proof (in ZFC, say, or some natural extension) of the formal sentence "$P$ defines a well-ordering." Does there exist such a $P$, and does that answer relate to the independence result mentioned above?

More generally, we can consider an existential set-theoretic statement $\exists P: F(P)$ where $F$ is some set-theoretic formula. Looking to the previous example, $F(P)$ could be the formal version of "$P$ defines a well-ordering on $\mathbb{R}$." (We would probably begin by rewording that as something like "for all $z\in P$, $z$ is an ordered pair of real numbers, and for all real numbers $x$ and $y$ with $x\neq y$, $((x,y)\in P \vee (y,x)\in P) \wedge \lnot ((x,y)\in P \wedge (y,x)\in P)$, etc.) On the one hand, such a statement may be a theorem of ZF, or it may be independent of ZF but a theorem of ZFC. On the other hand, we can ask whether there is an explicit set-theoretic formula defining a set $P^\*$ and a proof that $F(P^\*)$ holds. How are these concepts related:

  • the theoremhood of "$\exists P: F(P)$" in ZF, or its independence from ZF and theoremhood in ZFC;

  • the existence of an explicit $P^\*$ (defined by a formula) with $F(P^*)$ being provable.

Are they related at all?

| cite | improve this question | | | | |
  • $\begingroup$ I think I'm a bit confused about what you mean by "explicit". Can you clarify whether, for you, the statement "there exists x such that blah" and the statement "there exists an explicit x such that blah" mean the same thing or different things? I think that for you these are different concepts but I'm struggling to formalise the difference. $\endgroup$ – Kevin Buzzard Nov 13 '09 at 9:39
  • 4
    $\begingroup$ Here's a related question. I once saw as an UG a proof that the set of positive reals x such that sin(x)=0 contained a smallest element, and I then saw a definition of pi: it was the smallest x>0 such that sin(x)=0. Is that an "inexplicit" definition of pi? If I instead define pi to be the limit of an infinite series, and then invoke some abstract epsilon-delta theorem that says that infinite series for which the terms decrease rapidly have a unique sum in R, is that then an "explicit" definition of pi? Can someone better versed in logic than me explain the logical point behind the difference? $\endgroup$ – Kevin Buzzard Nov 13 '09 at 9:47
  • $\begingroup$ In my example, "there exists a well-ordering on $\mathbb{R}$" is a statement (indeed, theorem) of ZFC. On the other hand, "there exists an explicit well-ordering" is not a statement of ZFC: it's a statement about ZFC, that there is a formula of ZFC defining a set that is provably a well-ordering. $\endgroup$ – Darsh Ranjan Nov 13 '09 at 9:51
  • 1
    $\begingroup$ @buzzard, regarding your second comment - those are both explicit definitions, since you can prove that they define unique objects. $\endgroup$ – Darsh Ranjan Nov 13 '09 at 9:54
  • $\begingroup$ One way to make Darsh's question precise would be to ask whether there is a relation on R given by a formula in the language of set theory, which can be shown to be a well defined order without using choice, and which is a well-ordering in the presence of choice. $\endgroup$ – David E Speyer Nov 13 '09 at 12:07

In Goedel's proof of consistency of AC, we in fact get much more. There is an explicit relation defined, which is (provably in ZF) a well-ordering of a certain subset of the reals. It is consistent (and follows from the axiom V=L) that the subset is all of the reals.

| cite | improve this answer | | | | |
  • $\begingroup$ Thanks. If I've interpreted this correctly, this means that there is an explicitly defined relation that, in ZF+constructibility, can be proved to well-order the real numbers. This probably generalizes to all constructible sets, right? (Sorry, I'm not all that familiar with the constructible universe and such.) $\endgroup$ – Darsh Ranjan Nov 13 '09 at 21:26
  • $\begingroup$ Yes, in fact L has an explicit well-ordering, so if V=L that means there is an explicit well-ordering for the universe. Of course V and L are proper classes, so you have to say it properly... $\endgroup$ – Gerald Edgar Nov 13 '09 at 21:41
  • $\begingroup$ This seems to be the right answer to my question, then (though I think I may not have asked the right question). $\endgroup$ – Darsh Ranjan Nov 14 '09 at 5:09

Levy has a few interesting things to say on the definability of a set whose existence requires the axiom of choice, see pages 171- 175 Basic Set Theory, Perspectives in Mathematical Logic. In particular, he mentions Feferman's result on the unprovability in ZFC of the existence of definable well ordering of reals.

On your last question: Levy mentions an example (exceedingly trivial) of a formula F(x) for which one does have a definable set satisfying it in ZFC although the existential formula "for some x, F(x)" is unprovable in ZF.

| cite | improve this answer | | | | |
  • $\begingroup$ You can find Feferman's paper here: matwbn.icm.edu.pl/tresc.php?wyd=1&tom=56. The relevant result is Theorem 4.9, I believe. (A minor addition to Ashutosh's answer: It's consistent with ZFC+GCH (not just ZFC) that there is no definable well-ordering of ℝ.) $\endgroup$ – Zach N Oct 14 '11 at 13:09
  • $\begingroup$ @ZachN, I think they've done some jiggering to the website since you posted that link. Is the paper Feferman - Some applications of the notion of forcing and generic sets? $\endgroup$ – LSpice Oct 8 '17 at 23:56

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.