Skip to main content
3 of 9
added 55 characters in body
Joel David Hamkins
  • 236.4k
  • 44
  • 777
  • 1.4k

The bold statement is not true in the generality in which you state it.

But let's get a little more clear on what you mean. One does not formally use axioms at all in a definition, but rather in a proof. To define an object means to provide a statement $\varphi(x)$ that one and only one object satisfies. What one means by not using an axiom in a definition, is that in order to prove that the statement does in fact define something, we do not need to use that axiom. Or perhaps one has in mind a constructive procedure, but this is really just a sequence of such definitions. Such a construction could be said to not use the axiom of choice, if at every step, in every model of ZF, the definition succeeds in defining a unique object.

It is easy to make a counterexample, now, by the definition: let $f$ be the characteristic function of the $L$-least non-measurable set of reals in $L$.

This definition does not use the axiom of choice, since it is sensible as a definition in any model of ZF, and picks out a unique function on the reals in any model of ZF. But it is not provable in ZF that this function is measurable, since if $V=L$, then $f$ is definitely non-measurable.

Meanwhile, it is consistent with ZFC that the set of all reals in $L$ is countable in $V$, and in this case, the function $f$ is the characteristic of a countable set, and hence measurable in $V$.

So the definition, which did not use the axiom of choice (since it works as a definition in any model of ZF), sometimes defines a measurable function and sometimes does not, in the various ZF worlds.

At the end of your post, you seem to suggest that, ("clearly") if a definition defines a measurable set in some model of ZF, then it defines a measurable set (in our current ZFC universe). But this is not quite right. One can write down a definition $\varphi(x)$ that ZF proves defines a unique set of reals, but the set of reals defined is measurable in an inner model and non-measurable in a larger model.

Lastly, let me mention that there is another sense in which something very like your bold statement is true, and so actually you are not too far off, if you adopt the perspective and philosophy of large cardinal set theory. Namely, if there are sufficient large cardinals, then it follows that every projectively definable function or set of reals is Lebesgue measurable. A projectively definable set is one that defines the set or function by quantifying only over the reals and the integers and the basic algebraic operations and orders there. It goes beyond projective, and I see now that Andres has posted some further links on this.

Joel David Hamkins
  • 236.4k
  • 44
  • 777
  • 1.4k