Are sets constructed using only ZF measurable using ZFC?

Suppose $S$ is a subset of $\mathbb{R}$ which can be defined without using the axiom of choice, i.e. which can be proved to exist using only the axioms of ZF. Does it follow that $S$ is measurable?

We know that ZF + "All subsets of $\mathbb{R}$ are Lebesgue measurable" is consistent (assuming ZF is), but the claim doesn't follow from this alone, since there could be a proof that $S$ is not measurable which uses choice.

-
This is an interesting question, but it lacks a bit in formulation. In ZF one cannot even prove the existence of non-Borel sets. However in a universe where all sets are Borel these set can be quite strange. – Asaf Karagila May 8 '12 at 4:36
This is either a nitpick or a lack of understanding the question on my side, but wouldn't sets such that their existence can be shown be more precise wording than set which can be defined? I can write down the definition of Vitali set without any use of AC, but to show that such a set exists, I use AC. – Martin Sleziak May 8 '12 at 4:46
BTW wouldn't set-theory or axiom-of-choice (or both) suitable tags for this question? – Martin Sleziak May 8 '12 at 4:48
@MartinSleziak: I agree. Done. – Ross Millikan May 8 '12 at 4:52
Presumably, the nature of "defines" is something like: Give a statement $P(X)$ with one unbound variable $X$, such that you can prove in ZF: $(\exists X:P(X)) \land (\forall X,Y:P(X) \land P(Y)\implies X=Y)$ – Thomas Andrews May 8 '12 at 4:56

Perhaps surprisingly, the answer to your question is no. But "morally" the answer is yes.

To see the "no" answer, there is a formula $\phi(x)$ such that a real $r$ satisfies $\phi$ iff $r$ is in the constructible universe $L$. Similarly, there is a formula defining a well-ordering $<_L$ of $L$, and therefore there is a formula $\psi$ such that $\psi(r)$ holds iff $r$ is a real in $L$, and it belongs to the $<_L$-first non-Lebesgue measurable subset of ${\mathbb R}$ in $L$. Such a set exists, since (provably in ZF) $L$ satisfies ZFC, and it is a theorem of ZFC that there are sets that are not measurable.

Now, it is consistent with ZF that $V=L$, that is, that every set is constructible. But then the set of reals defined by $\psi$ would not be measurable. This shows that one cannot prove in ZF (or ZFC) that any ZF-definable set of reals is measurable.

On the other hand, one of the most significant results in set theory is the theorem of ZFC + large cardinals that any reasonably definable set of reals is measurable; for example, any set of reals in the universe $L({\mathbb R})$, and this certainly includes all sets "naturally definable".

This first appeared in the Martin's maximum paper by Foreman, Magidor, and Shelah, where a supercompact was used, and was later refined in a paper by Woodin and Shelah, where the key notion of Woodin cardinals was isolated. [Note this is not just a consistency statement. It is a fact about the universe of sets, in the presence of sufficiently large cardinals.]

Moreover, it is consistent (but not provable) with large cardinals that any ordinal definable set of reals is measurable, carries all the usual regularity properties, etc, and in fact somewhat more. (This is usually stated nowadays in terms of determinacy.)

Our current understanding is that the "definable" or well-behaved sets of reals are the universally Baire sets. (In the presence of enough large cardinals) they are certainly measurable and in fact have all the usual regularity properties (for example, they are countable or of the same size as the reals, and they all have the property of Baire. In fact, they are determined).

-
I thought that with sufficiently many large cardinals projective sets were determined in $V$, and determined implies measurable. (By the way, this is one of the most amazing connections in set theory between small sets and large cardinals.) – Asaf Karagila May 8 '12 at 7:12
Hi Asaf. Yes, that's correct. – Andrés Caicedo May 8 '12 at 14:05