Is the well-ordering in the well-ordering axiom required to be definable?

Question

It is well-known that Axiom of Choice is equivalent to the statement that every set can be well-ordered. Now, to show that $M\models AC$, is it sufficient to show that there exists some well-order of every $x\in M$ inside $V$, or does the well-order have to be an element (or maybe just subset?) of $M$?

My question arises from the fact that to show that Gödel's constructible universe $L$ satisfies $AC$, some simply define an order relation and prove that it's a well-order of $L$ (implying thus that every set can use this well-order, proving the well-ordering axiom), where others take the trouble to also show that the order relation (restricted to some $x\in L$) is in fact inside $L$ and satisfying that $L$ itself thinks that it's a well-ordering. Is the first group of people missing this bit, or is the second group "overproving" it?

Answer 1

The well-ordering theorem states that

for every set, there is a relation which well-orders it.

When speaking about a model $M$, in order to conclude that $M\models \mathsf{WOT}$, like any similar statement, we must show that for each $x\in M$ that there is some $R\in M$ such that $M$ "thinks" that $R$ well-orders $x$. (Just unwind the definition of $M\models\phi$ for the appropriate $\phi$.)

Similarly, to show that $M$ satisfies the Power Set Axiom requires that for each $x\in M$ there be some $X\in M$ which $M$ "thinks" is the power set of $x$.

Whether this $R$ is definable or not is often beside the point as far as $M$ satisfying $\mathsf{WOT}$ is concerned ($\mathbf{L}$ being perhaps an outlier based on the nature of the constructible universe), but in certain circumstances in is interesting to determine which sets have definable well-orders; the reals being of particular interest. Even then, determining the complexity of such a well-order is of further interest. (Also of interest is what extra properties a model can have (e.g., $\mathsf{MA}$) in conjunction with having a definable well-order of the reals of a specified complexity.)

(Think of the interest in definability as sort of saying that not only is there a solution to some equation, but additionally there is a nice solution.)

Answer 2

The trouble with the word "definable" is that it's very unclear what people mean if the context is not fully set.

If you mean "definable in the language of set theory without parameters", then the answer is strictly no. By forcing we can add two real numbers $a,b$ in such way that no parameter free formula can order the set $\{a,b\}$.

Perhaps you mean definable with parameters. But then consider just a bijection with a set $A$ and an ordinal. We can prove that such a bijection exist, therefore using it we can define a well-ordering of $A$. But that's circular, so that can't be right.

We can talk about other sort of parameters, but they will usually go through either circularity (i.e. we use something which is essentially a well-ordering of the set to begin with) or that we can show them to be false using arguments like forcing.

It is true, however, that $M\models\sf AC$ if and only if for every $x\in M$ there exists a set of ordinals $E\in M$ such that $x\in (L[E])^M$. So we can say that $x$ has a well-ordering definable from a set of ordinals, but we can usually take this set of ordinals to be some clever way of encoding $x$ into ordinals, so we run into circularity again.

The reason that Godel's universe has a parameter free definable well-ordering is that in order to prove that the axiom of choice is consistent to begin with, you need to show that there is some model where the axiom of choice holds. And if you want that, it's easiest to show that you can define it straight up. But once you know that it is consistent and you no longer care about the universe, as long it satisfies the axiom...

Well, in that case you don't have to worry about definability anymore.