This is a reply to Jay’s comment.

First, I should mention that in the absence of AC, the real numbers may not be well-orderable at all. In the Solovay model of ZF in which every set of reals is Lebesgue-measurable, for instance, the reals cannot be well-ordered, since one can construct from a well-ordering of the reals a non-measurable set of reals (by choosing a transversal of . Exercise!).

There are at least two interpretations of ‘explicit’ in this context. I’ll address the two that seem most natural to me: Borel/projective and definable (by a first-order formula).

The Axiom of Constructibility says that , or that every set is constructible. (The class is the class of all sets, and is the class of all constructible sets.) The axiom might seem appealing to the non-set-theorist, since it implies the Axiom of Choice and the (Generalized ~~even, I think~~) Continuum Hypothesis. In fact, this is how Gödel originally proved the relative consistency of AC: by showing that AC holds in , which is a model of ZF. It’s also important to realize that is the *smallest* inner model of ZF (that is, in a model of ZF, ‘s is the smallest model of ZF inside ): it contains only those sets which must exist because they’re forced to by the axioms (maybe something like the trivial group for the axioms of group theory). But assuming makes for a pretty ~~uninteresting~~ (limited, at least) set theory, and it’s therefore generally unappealing to set theorists. I would compare the restriction of set theory to ZF + (V=L) to the restriction of group theory to abelian group theory: the latter would make group theory (mostly) uninteresting and eliminate many tools useful to the non-group-theorist. It’s still useful to consider, though, especially for consistency business.

Aside: So, some Grothendieckian algebraic geometry depends on one or more large cardinal axioms, which are almost certainly inconsistent with V = L. (Edit: I think algebraic geometers need only assume something like *There is a proper class of inaccessibles*, which is considerably milder than what forbids.)

So the point of telling you about was to tell you this: if , then the whole set-theoretic universe is well-ordered, so (and every other set) inherits a well-ordering from the universe. One might hope for a Borel well-ordering of (Borel as a subset of , of course). I’m fairly certain that this is impossible (and that shouldn’t be hard to see, but I don’t see it right now). There are broader families of ‘explicit’ sets of , though; what we’re interested in is the projective hierarchy, described here. The punchline is that under the assumption , there is a well-ordering of the reals of complexity ; essentially, this means that, for some analytic set in , the well-ordering is the complement of projected down to . (*Analytic* means the continuous image of a Borel set.) So that’s fairly explicit, right? There have been other attempts at finding projectively uncomplicated well-orderings of the reals; see this answer to an MO question. But that’s under the assumption . Under certain large cardinal assumptions, the lower bound for the complexity of a well-ordering of is higher than .

The other natural interpretation of ‘explicit’ is ‘definable’. Your question then becomes something like, Is there some formula such that the set is a well-ordering of the reals? And the answer is that this is independent of ZFC+GCH. (And your question in this form is similar to this MO question. You’ll notice that I provide a link in my comment on that page to a paper by Feferman, in which he proves this independence.)

I think all this is accurate; I hope it’s helpful.

Interesting stuff. Confusing to me, but interesting. I do like the constructibility question and hope that all sets are constructible (sorry). I’d have to think about the projective business for awhile longer to understand it. One question that I do have: What do you mean by the existence of a formula which is a well-ordering of the reals? Do you mean formula in a way that differs from function? If a well-ordering exists, isn’t there implicitly a function which does it? With choice, probably. I thought that any sort of process can be described with a function that maps where it starts out to where everything ends up.

What do you mean, you “hope that all sets are constructible”?

A formula like iff . This defines the diagonal line that is the graph of the function . Not every set is necessarily definable, though. Definability depends on the (formal) language you’re using, too; for instance, you won’t get very far trying to define subsets of using only (regular logical connectives and) the symbol . If you add the symbols , though, you can define quite a lot.

So when I said 'definable' up there, I meant 'definable in the language of set theory', which includes the symbol .