This question actually consists 3 related pieces of text, which I've gathered under this title about which I would like your opinion (they rather contain the implicit question "is this the right way to think about this issue"). I'm willing to offer bounty for this.
$1.$ Consider the following theorem: There is no function $f:\mathcal{P}\left(\mathbb{R}\right)\rightarrow\left[0,\infty\right]$ that is translation-invariant and $\sigma$-additive such that $0<f\left(\left(0,1\right)\right) < \infty$.
Its proof goes like this: We first define a equivalence relation $a\sim b:\Leftrightarrow a-b\in\mathbb{Q}$ on $\mathbb{R}$, then select a system $S$ of representatives from it that lies in $\left(0,1\right)$. This $S$ is then the key to prove the theorem.
What I'm concerned with is how we obtain $S$. The proof I know says "we have to use the axiom of choice to do that'': The choice function picks member from every an equivalence class. As I understand it the use of the axiom of choice comes from the fact that we can't determine explicitly the form of the set all the equivalence classes (if we have one representative we can easily get one that lies in the open unit interval).
Each equivalence class has to have the form $a+\mathbb{Q}$ for some real $a$ and it is clear that the equivalence class of any rational number is $\mathbb{Q}$. But the irrational numbers cause problem: We have no means to explicitly describe all equivalence classes of irrational numbers, since for a given $b,c\in\mathbb{R}\setminus\mathbb{Q}$, we don't know if they are in the same equivalence class or not: $1+\sqrt{2}$ and $2+\sqrt{2}$ obviously are; but for $\pi$ and $e$ we don't know, since currently it is unknown whether $\pi-e$ is rational or not. Now the axiom of choice circumvents this issue. But the need to use the axiom of choice seems to me to depend in this case only on present state of research: Maybe in 100 years we will settle the case for $\pi$ and $e$ and moreover devise some methods such that for given $b,c\in\mathbb{R}\setminus\mathbb{Q}$ we know if they are in the same equivalence class or not (for example if it turns out that we can somehow classify them we can distinguish by cases). Therefore saying we have to use the axiom of choice seems bad to me; saying "presently we cannot do without the axiom of choice" seems better.
$2.$ The above seems to me to be in contrast to saying "we have to use the axiom of choice to exhibit a functions that picks an element from every subset of the reals" since I read, that there there are strong model-theoretic arguments that imply that indeed no one will ever be able to explicitly construct such a function. But even in this case it seems to me, that the word "have" is too strong, since it implies that one can somehow prove that without the axiom of choice it is impossible to prove that statement.
$3.$ Is proving, that a statement $T$ cannot be proven without the axiom of choice the same as proving that $T$ is equivalent to the axiom of choice ?
Do you agree with me ?
Let me answer in three parts.
We when we say that we need to use the axiom is not because for some numbers do know and for some with don't know what is their equivalence class. There are models where the axiom of choice fails and it is impossible to choose representatives from $\Bbb{R/Q}$.
This is why we need the axiom of choice, and will always need it, in order to construct a non-measurable set such as a Vitali set. It is not about our lack of knowledge about the explicit real numbers and so on, it is simply because we know that it is consistent that it is impossible to do if the axiom of choice fails.
Yes. We can prove that in some models it is impossible to make this choice, for example there are models where all the sets are in fact Lebesgue measurable, and there are others where all the sets are Borel. In both these models we have that (1) the axiom of choice fails, and (2) there is no choice function from $\Bbb{R/Q}$.
No. It is not the same thing. To see it more clearly observe that the axiom of choice is much stronger than the axiom of countable choice (choice from countable families of non-empty sets). But it is fine to say that you cannot prove the axiom of countable without some form of the axiom of choice. That is to say, we cannot prove it from the rest of the axioms of ZF. It does not mean that we can prove the axiom of choice if we have the axiom of countable choice at our disposal.
Similarly the fact that we cannot prove the existence of a non-measurable set, or in particular a Vitali set, without some form of the axiom of choice does not imply that we can prove the axiom of choice from the existence of such set.
The rule of thumb is that if a statement is talking about a concrete set (in our case, $\Bbb R$, or $\cal P(\Bbb R)$ if you prefer) then it will not imply the axiom of choice. Why? Because we can arrange a model where the axiom of choice holds for sets far larger than this one, and then breaks in the most acute way possible.
You might also be interested in: Axiom of choice, non-measurable sets, countable unions