We cannot write this function 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.
 A: 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:


*

*How do we know we need the axiom of choice for some theorem?
A: One can show that such a function cannot be found not only in ZF but even in ZF+(countable choice), as follows.
For simplicity let's discuss a closely related problem where the space is not $\mathbb{R}$ but rather the circle $\mathbb{R}/\mathbb{Z}$. One approach that immediately comes to mind is to use the results of the following paper:
Solovay, R. A model of set-theory in which every set of reals is Lebesgue measurable. Annals of Mathematics (2) 92 (1970), 1--56.
If you had a way of specifying such a set $X$ without uncountable choice, in Solovay's model it would be measurable and one would then get a contradiction by considering two cases: (a) if the measure of $X$ is zero then one would use countable additivity of Lebesgue measure (which follows from countable dependent choice) to show that the measure of the circle is zero; (b) if the measure of $X$ is nonzero then the measure of the circle would be infinite.  In either case one gets a contradiction, allowing one to conclude that such a set does not exist.
A: A possible notion in set theory that may correspond to your "writing by hand" is that of ordinal definable sets. But then, the existence of ordinal definable choice function of $\mathbb{R} / \mathbb{Q} $ is independent over $ZFC$. For an elementary exposition to this notion start with Levy's "Basic set theory" and then maybe look at Jech, Kanamori or even better original papers of Solovay and Shelah. 
Here are the references:
Solovay, Robert M. (1970), "A model of set-theory in which every set of reals is Lebesgue measurable", Annals of Mathematics. Second Series 92: 1–56
Shelah, Saharon (1984), "Can you take Solovay's inaccessible away?", Israel Journal of Mathematics 48 (1): 1–47
