Definable Models Without Choice

Suppose that a parameter formula defines an inner model. Does that inner model satisfy choice?

Well, obviously, if choice failed then the answer is no, just by taking \(x=x\). But what if we remove that option. Namely, if the inner model is not the entire universe, then choice holds.

That sounds like a very plausible scenario. After all, there are constructive mathematics systems in which the principle "if we can construct a family of sets, then we can choose from them" holds. And it makes sense. If a formula \(\varphi(x)\) defines an inner model of \(\ZF\), then in some way, we expect it to be an inner model of \(\ZFC\).

But let me take a slightly broader interpretation: Can there be a model of \(\ZF\) such that there is a formula \(\varphi(x)\) (without parameters!) such that \(\varphi\) defines an inner model where the axiom of choice fails?

Well, much to my surprise, the answer is indeed positive.

Starting from \(V=L\), add a Cohen real \(c\), which adds a set \(X\) such that \(L(X)\) does not satisfy the axiom of choice (in fact, going through the Bristol model construction, there is a proper class of these sets which result in different models). Next, code the Cohen real into \(\HOD\). Namely, force that \(c\) is ordinal definable (e.g. by coding it into the continuum function below \(\aleph_\omega\)). Since \(\HOD\) admits a definable well-ordering, we can ask what is the least set \(X\) such that \(L(X)\) does not satisfy the axiom of choice (or equivalently, what is the least \(X\) such that the transitive closure of \(X\) does not have a definable well-ordering). But this creates a parameter-free formula \(\varphi(x)\) which defines the model \(L(X)\) for the least \(X\) (in the \(\HOD\) well-ordering) for which \(L(X)\) is not a model of \(\ZFC\).

I find this sort of thing to be interesting, since definable "models" are almost exclusively models of choice. This is because we think about stuff that we can "hereditarily define" as stuff we can somehow construct by hand, and thus deduce the axiom of choice from. But the above example shows that in fact this is a second-order thinking, and through first-order approach only, one can end up with a parameter-free definable model in which the axiom of choice fails.

Remark: David Asperó noted that \(L(\RR)\) is another example, e.g. under large cardinals or after adding \(\omega_1\) Cohen reals. It is perhaps a simpler solution, but the above still provides a nice and "canoincally non-canonical" model of non-AC.