We know that non measurable sets in $\mathbb{R}$ exist, relative to the Lebesgue measure, but for finding one we need the Axiom of Choice. So I was thinking, maybe every time we need to prove measurability of a set, we could say that we didn't need the Axiom of Choice for constructing that set? For example, take two measurable functions $f,g:\mathbb{R} \to \mathbb{R}$. We know that $$\left\{x \in \mathbb{R} \mid f(x) =g(x) \right\}$$ is measurable. Could we prove it just saying that we didn't use the Axiom of Choice to build that set?
Thanks for your answers.
Edit
To be more precise, my question is : if we make operations starting from some sets that are measurable or measurable functions, then we can conclude measurability just noticing that we haven't used the axiom of choice? (If we actually didn't)
There's definitely something along these lines we can do, but it's surprisingly difficult to do exactly: we need to talk about different "universes" in which our mathematics takes place, and how we can transfer facts between them appropriately. Unfortunately, the following answer is rather technical - that's sort of the point, that technical issues are essential here - but hopefully I've managed to pare things down to the point that it's actually interesting:
The key idea here is that of an inner model (of ZF + whatever). The precise definition of the term is rather technical ("a transitive proper class satisfying the ZF axioms (+ whatever)"), but the intuition is that it's just a more restricted universe for doing math, which - by virtue of being more limited - might have nicer properties. (An inner model could also be much worse of course, but we're only going to be interested in the nice ones for now.)
Under reasonable set-theoretic assumptions (so-called "large cardinal hypotheses"), there are lots of inner models $M$ with the following properties:
$M$ satisfies ZF + DC (= a weak choice principle which prevents really stupid stuff from happening) + "Every set of reals is measurable."
Every real number is in $M$.
If $X\subseteq\mathbb{R}$ and $X\in M$, then $X$ is measurable.
(That third condition actually comes for free from the second, but that takes an argument.) We will call such models "nice."
The initial idea is that when we write a definition $\varphi$ of a set $S$ in the "real world," we can "copy" that definition in a nice inner model $M$ containing those parameters to get "$M$'s version of $\varphi$" - which I'll call "$\varphi^M$" - and by the niceness of $M$ conclude measurability of the original set.
Unfortunately, we've got problems.
Our first issue is that our original definition $\varphi$ might involve some parameters - e.g. $\{x: f(x)=g(x)\}$ involves $f$ and $g$. Now we can't "run that definition inside $M$" unless $M$ also contains $f$ and $g$. So we can't use any old inner model.
Much worse, however, is the following: when we switch from the "real world" to an inner model, definitions go wild. For example, consider the definitions "$\{x: x\not=x\}$" and "$\{x:$ $x=17$ and the axiom of choice fails$\}$." In reality, these each correspond to the same set, namely the emptyset. But now suppose $M$ is a nice inner model. $\{x: x\not=x\}^M$ still defines $\emptyset$, but $\{x:$ $x=17$ and the axiom of choice fails$\}^M$ defines $\{17\}$ (since $M$ thinks the axiom of choice fails).
So here's what we need to do to make everything work. Suppose we have a definition $\varphi$ (using "parameters" $a_1,...,a_n$) of a set of reals $S$, and we want to show that $S$ is measurable.
First, we show that $\varphi$ is absolute: if $M$ is any nice inner model and $r$ is a real number, then $M$ thinks $r$ is in the set defined by $\varphi$ iff $r$ really is in the set defined by $\varphi$. (This isn't a given! Besides the toy example above, there are more serious examples: e.g. as Andreas mentions, it's possible that there is a fully-definable non-measurable set; so even if choice isn't involved explicitly in $\varphi$, "choiciness" could still play a hidden role.)
Next, we show that there is a nice inner model $M$ with $a_1,...,a_n\in M$. (This also isn't a given! For a trivial example, suppose one of the parameters is itself a non-measurable set.)
The second step lets me "run $\varphi$ inside $M$;" the resulting set of reals ("$M$'s version of $S$") is measurable, and by the first step that set is the actual $S$ we care about. We can also use this approach to prove "template" theorems, applying to many definitions at once.
However, all of this takes serious work, and relies on set-theoretic hypotheses beyond ZFC. The end result is:
Does that mean that "definition-examination" is never helpful to prove measurability?
Not at all! But we have to be more fine-grained in our examination, and look at the syntactic complexity of the definition: syntactic complexity is connected to topological complexity, and so we can sometimes argue that a set is measurable by saying something like: "The definition of this set has such-and-such syntactic form, so it's (say) Borel, and all Borel sets are measurable." This is part of descriptive set theory.