I'm a new user so if my question is inappropriate, please comment (or edit maybe).
If we accept axiom of choice, we can find a choice function for $\mathbb{R} / \mathbb{Q} $ , this is obvious. But we cannot find such a function "with hand and I think we should prove we cannot. My question is how can we prove such a thing or how can we define "writing with hand"? This question might be generalized but because I'm not so sure about it, I will stuck in that example.
I think my work for this question is unnecessary but I think I should share some of it.
First of all:
$ZFC$ $\Rightarrow$ Every $\alpha \in \mathbb{R} / \mathbb{Q} = \{ r + \mathbb{Q}: r \in \mathbb{R} \} $ there exists a set $X \subset \mathbb{R}$ such that $|\alpha \cap X| = 1 $
I tried to approach to question in such a manner but then I believed that proof or explanation must be in meta-mathematics. We can approach this by assuming that we can find such a function in $ZF\neg C$ and prove that we are pope. But I'm not satisfied with this strategy.
Most satisfiable and probable strategy that I thought is trying to show that if we want to write this function with hand (and not with technology like axiom of choice) we should use infinitely many characters.
Thanks for any help and please bear in mind that I cannot understand high-level explanations.
When we have a statement "There is some object with property $\varphi$". Often we can prove this statement using the axiom of choice. When we say that "we cannot write a definition of such object by hand" we often mean that we cannot prove the existence of this object without some appeal to the axiom of choice. Yes, this is quite informal and ill-defined, but so are "by hand" and "explicitly".
There are two common methods to showing something like that:
The reduction to another problem. We prove that given such object, we can generate another object, which we may assume doesn't exist without some choice. For example, a non-measurable set. Another example is a linear ordering of $\Bbb{R/Q}$.
The problem with this approach is that it relies on previous knowledge, and the more extensive your knowledge of choice principles is, the easier or harder it can get.
Exhibit a model. We know from the completeness theorem that $\sf ZF$ can prove a statement if and only if it is true in all its models. We already know that in models of $\sf ZFC$ the statement is true, so now we need to check and see what happens in models where the axiom of choice fails. What you have to do here is to construct a model of $\sf ZF$ where our statement fails. Of course this implies that the axiom of choice must fail in the model as well (or else $\sf ZF$ was inconsistent to begin with).
Note that the failure of the axiom of choice is not necessarily equivalent to the failure of our statement. It is a byproduct of its failure. Since the statement is a consequence of the axiom of choice, the failure of choice is a consequence of the failure of our statement.
This method is difficult. It often employs advanced set theoretical methods such as forcing. It is, however, important to understand why this method works at all.
In the case of the statement "there exists a choice function from $\Bbb{R/Q}$" we can either rely on the construction of Solovay, or others, which proved that there are models in which the Lebesgue measure has properties which are incompatible with such choice function.
Or you can try and construct a model yourself.
Also related: