In ZFC, the existence of a well-ordering of the reals is provable, being equivalent to AC. Fine. If, in addition, one assumes V=L, one can well-order them by well-ordering the formulas. A bit harder, but OK. However, if you assume the existence of non-constructible reals, is it possible that one could prove (how, I do not have a clue) that every set which well-orders the reals is a non-constructible set, and therefore cannot be explicitly exhibited? Or, although no one has yet come up with an explicit well-ordering of the reals, is there any hope that an explicit well-ordering is theoretically possible?
Oops. I accidentally omitted "WO" in the sentence. That should have read, "In ZFC, the existence of a well-ordering of the reals is provable, WO being equivalent to AC." Not, as you rightly pointed out, just the well-ordering of the reals.I doubt that the mere assumption that the reals have a well ordering implies AC.
Again, that was rather sloppily expressed, but I was referring to the following:L, one can well-order them....What proof in particular are you referring to?
Constructible universe - Wikipedia, the free encyclopedia
The other two parts were sloppy introductions, which I apparently had best left out, to this question. So thank you, MoeBlee, for this precise answer. As I am do not have access to a print version of Levy's book, then I will hope that I can find that somewhere: perhaps in Basic set theory - Google (not certain, since some pages are omitted). But as this omits much of the index, then in case you have the page number, that would be highly appreciated. Thanks again.As far as I understand, the answer is 'no'. A result of Feferman is that no explicitly defined well ordering of the real exists. This is mentioned in Levy's 'Basic Set Theory'.
I don't have the book with me today. I'll try to remember to bring the book with me tomorrow to quote from it and give you the page numbers and the reference to the original paper.
Paraphrasing from 'Basic Set Theory' by Levy, pg. 173 ['P' for power set; 'w' for omega]:
One cannot prove in ZFC that there is a definable x that satisfies "x is a well ordering of Pw"
by Feferman "Some applications of the notions of forcing and generic sets" in Fund. Math. 56, 325-345 (1965).
I don't think it's crucial in this context whether we couch this in terms of R (the set of reals) or in terms of Pw.
However, in certain other respects, what I said is different from what Levy reports there, but, given some reasonable understanding of the vocabulary, I think we could get my statement from Levy's.
I grant though, that I've not worked out for myself a fully precise understanding of this subject of "definable sets".
In any case, Levy's discussion is pages 171-176.