Explicit construction of a nonmeasurable set, where only the proof of correctness uses choice?

Question

By Solovay's theorem, assuming the existence of an inaccessible cardinal, the axiom of choice is necessary to prove the existence of nonmeasurable sets. In the past, I've thought that one consequence of this theorem is that if I construct a set without using choice (or even merely using dependent choice), then I don't have to worry about it being nonmeasurable.

But now I realize that I was making an unjustified assumption. I'm not sure what the appropriate way to precisely phrase this question is, but I'm wondering: is there a non Lebesgue measurable set $E \subseteq \mathbb{R}$ which can be explicitly defined? I'm imagining that perhaps $E$ can be defined without invoking choice (unlike Vitali sets or their cousins), but then proving that $E$ is nonmeasurable requires choice. Is this possibility also ruled out by Solovay's theorem somehow?

Answer 1

If you can prove that your definition defines something, then will in particular define something in Solovay's model, and that something will in particular not be a nonmeasurable set.

So the best you can hope for is an explicit definition of a subset of $\mathbb R$, such that the thing defined will in some models of ZF be a nonmeasurable set.

And this is in fact the case: Since pointwise definable models of ZFC exist, such a model will contain a nonmeasurable set and that set will have an explicit definition in the language of set theory. (In fact, as Asaf points out in comments, we don't need to appeal to pointwise-definable models here; there is a particular formula that picks out the first nonmeasurable subset of $\mathbb R$ in any model of $\mathbf V=\mathbf L$, where "first" is according to the global well-order, and this one formula will work for the $\mathbf L$ of every model of ZF).

We can even arrange that this particular definition always provably defines some subset of $\mathbb R$ -- if our element of the pointwise definable model is the only set that satisfies the formula $\phi(x)$, then $$ \{ y\in \mathbb R \mid \exists x: \phi(x)\land y\in x \} $$ will define some subset of $\mathbb R$ in every model, and it will at least sometimes be non-measurable.

Answer 2

From wikipedia: $\:$ "In particular Krivine (1969) showed there was a model
of ZFC in which every ordinal-definable set of reals is measurable, ..."
Therefore ZFC does not prove that there is a definable nonmeasurable set.

Using an explicit definable well-order on $\mathbb{R}\hspace{-0.04 in}\cap$OD to run a Vitali construction
gives an explicit set which won't be measurable if $\: \mathbb{R} \subset \hspace{.04 in}$OD$\;$.