In the constructible universe $L$, there is a definable well-ordering of the entire universe. This universe is built up in transfinite stages $L_\alpha$, and the ordering has $x\lt_L y$ when $x$ is constructed at an earlier stage, or else they are constructed at the same stage, but $x$ is constructed at that stage by an earlier definition, or with the same definition, but with earlier parameters. I also explain this in this MO answer.
One may extract from this definition a rather low-complexity definable well-ordering of the reals by capturing the countable pieces of the $L$ hieararchy by reals. That is, if $x$ is a real number of $L$, then it appears at some countable stage $L_\alpha$ for a countable ordinal $\alpha$, and the entire structure $L_\alpha$ is countable, and hence itself coded by a real. Here, we code a set by a real in any of the standard ways, for example, by coding a well-founded extensional relation on $\omega$ whose Mostowski collapse is the given set. Furthermore, the $L$-order is absolute to any $L_\alpha$, since $L_\alpha$ knows about the $L_\beta$-heirarchy for $\beta<\alpha$. Also, if a countable structure is well-founded and thinks $V=L$, then it is $L_\alpha$ for some $\alpha$. Note that if a real $z$ codes a first order structure $M$, then the question of whether $M$ satisfies a first order assertion is an arithmetic statement in $z$, since we need only quantify over the coded elements, which are coded by natural numbers.
Putting all this together, we get that the following are equivalent for any two reals $x$ and $y$:
- $x\lt_L y$ in the $L$ order.
- There is some countable ordinal $\alpha$ such that $L_\alpha$ satisfies $x\lt_L y$.
- For every countable ordinal $\alpha$, if $x$ and $y$ are reals in $L_\alpha$, then $L_\alpha$ satisfies $x\lt_L y$.
- There is a real $z$ coding a well-founded structure that thinks $V=L$ (and so this structure must be some $L_\alpha$) in which $x$ and $y$ are reals and the structure satisfies $x\lt_L y$.
- All reals $z$ coding well-founded structures $L_\alpha$ in which $x$ and $y$ are reals satisfy $x\lt_L y$.
The fourth statement has complexity $\Sigma^1_2$, since being-well-founded is $\Pi^1_1$. Similarly the fifth statement has complexity $\Pi^1_2$, so overall the ordering is $\Delta^1_2$.
The end result is that in the universe $L$, there is a low-complexity definable well-ordering of the reals. In this universe, therefore, all of the supposedly non-constructive applications of AC turn out to be completely definable.
