Concerning Borel measurability, it was already pointed out that there is an explicit formula s(x) such that ZFC proves "The set { x in R: s(x) } is not Borel". (This is not true for ZF, as was pointed out [elsewhere](http://mathoverflow.net/questions/32720/non-borel-sets-without-axiom-of-choice).) Concerning Lebesgue measurability, ZFC neither proves nor refutes the following: > There is an OD-definition (or: OD(R)-definition) of a subset of the reals which is non-measurable. There is a slight fuzziness here, because there are many non-equivalent notions of definability; OD(R)-definability is perhaps the most prominent and useful. But an explicit formula can be given: There is a formula phi(x) in the language of set theory (without parameters) such that ZFC neither proves nor refutes > "The set { x in R : phi(x) } is non-measurable". In fact, phi(x) can be of a rather simple form ($\Delta^1_2$, as you remarked above). Here is an abbreviated version of phi: For each real number x, let $x_1$ be the number obtained from x by deleting all even decimal places, $x_2$ by deleting all odd decimal places (do what you want for the countably many reals where this is not well-defined). This defines a measure-preserving Borel map from $\mathbb R$ to $\mathbb R\times \mathbb R$. Now consider the set M of all reals x for which there is some $\alpha$ such that $x_1\in L_\alpha$, but $x_2\notin L_\alpha$. ZFC does neither prove nor refute that M is Lebesgue-measurable. (I think that the fact that ZFC does not prove that M is measurable is already due to Gödel.)