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.