In some situations, you need to show Lebesgue-measurability of some function on $\mathbb{R}^n$ and the verification is kind of lengthy and annoying, and even more so because measurability is "obvious" because "why would it not be".
In such a situation, I have heard the argument: The function is clearly measurable, because the axiom of choice was not used to define it.
This argument makes some sense, because (as far as I know, I am not an expert) there are models of ZF (no C), where every function on $\mathbb{R}^n$ is Lebesgue measurable. So, suppose that we have a function $f$ in our model of ZFC constructed without the axiom of choice, then it is also a function in the model of ZF constructed above. Hence it is measurable there, and "clearly" all functions that are measurable in the model above are also measurable in our model.
But the question is: The bold statement above is very "meta". So how rigorous is this argument? Can it be made rigorous?
/Edit: I changed "Borel"- to "Lebesgue"-Measurable.
Best Answer
The bold statement is not true in the generality in which you state it. Nevertheless, something very like it is true, if one adopts the perspective and philosophy of large cardinal set theory and restricts the kinds of definitions that are considered.
First, 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 one can prove, without using that axiom, that there is such a unique object fulfilling the definition. Perhaps one has in mind a constructive procedure, but this is really just a sequence of such definitions, and such a construction does not use the axiom of choice, if at every step of the construction, the definition used at that step is a definition in any model of ZF.
One can easily make a counterexample, now, by the definition: let $f$ be the characteristic function of the least non-measurable set of reals in the constructible universe $L$, using the canonical definable well-ordering of $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 necessarily true in ZF that this function is measurable, since if the axiom of constructibility holds, that is, if we are living in $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, sometimes defines a measurable function and sometimes does not, in the various ZF worlds.
Let's give another concrete counterexample. The canonical well-ordering of the reals in the constructible universe $L$, mentioned by Andres, is a definable subset of the real plane $A\subset\mathbb{R}^2$, which in $L$ has complexity $\Delta^1_2$ in the descriptive-set-theoretic projective hierarchy. Thus, in our current universe $V$, the set $A$ has complexity at worst $\Sigma^1_2$, and so it arises from a certain definable closed subset of $\mathbb{R}^4$ by projecting onto $\mathbb{R}^3$, taking the complement, and then projecting to $\mathbb{R}^2$. So $A$ is definable in a highly concrete manner, without making any use of the axiom of choice. Nevertheless, it is not necessarily true that the resulting set is measurable, since inside the constructible universe itself, the resulting set is not measurable; in contrast, it is also consistent with ZF that there are only countably many constructible reals, and in this case the set $A$ would be countable and hence measurable. So the measurability of the set $A$ is not determined, despite the simple definition.
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 explain the sense in which your bold statement is on the right track. One of the truly surprising and remarkable discoveries of large cardinal set theory is that the existence of large cardinals has effects on fundamental mathematical truth at the level of descriptive set theory. In particular, the existence of sufficient large cardinals implies that every projectively definable set of reals is Lebesgue measurable. If there is a supercompact cardinal, and much less suffices, as explained in the article Saharon Shelah, Hugh Woodin, Large Cardinals Imply That Every Reasonably Definable Set of Reals Is Lebesgue Measurable, Isreal Journal of Mathematics, vol. 70, (1990) pp. 381-394 (reviewed by J. Bagaria in BSL 8:4(2002) pp. 543-545, as linked to by Andres in the comments), then every set of reals in $L(\mathbb{R})$ is Lebesgue measurable. The universe $L(\mathbb{R})$ consists of those sets that are constructible relative to reals.
So, if you assume large cardinals, and you define a set of reals by a definition that is absolute to $L(\mathbb{R})$ — and this is very likely the case if your definition works in ZF and does not involve set theory explicitly — then your set is Lebesgue measurable.
In particular, assuming that there are sufficient large cardinals, then every projective set of reals is Lebesgue measurable, and this may provide a soft sufficient criterion. The projective statements are those that can be expressed using quantifiers only over the reals and the integers, with the usual algebraic and order structure. Alternatively, the projective sets are those that you get by closing the Borel sets under continuous images and complements.
Let me point out that this kind of consequence of large cardinals is often pointed to by large cardinal set theorists as evidence that the large cardinal axioms themselves are on the right track, since they provide a such a rich, coherent and desirable structure theory for our everyday mathematics. We infinitely prefer the smooth and elegant descriptive set theory of large cardinals to the awkward land of counterexamples provided by the axiom of constructibility $V=L$.