Is it true ZF can't prove there is a choice function on the Turing degrees? It is possible to show there is no Borel choice function on the Turing degrees. In fact we can even prove there is no Turing invariant Borel injection from $2^\omega$ to $2^\omega$, which sort of says that there is no injection from the Turing degrees into $2^\omega$. The proof relies on the measurability of Borel functions.
Now using some strong large cardinal-like axioms such as "every set is determined", one can show that there is no choice function at all on the Turing degrees. With much lower large cardinal assumptions, Solovay built a model of ZF in which every set is measurable. I'm not entirely sure, but it is probably the case that there is never a choice function on the Turing degrees in such models.
My question is : has anyone succeeded in building a model of ZF in which there is no choice function on the Turing degrees (or maybe on simpler equivalence relations, such as being equal almost everywhere), without using large cardinal assumptions ? or maybe such a thing known to be impossible ?
 A: Here's an easy solution for the $E_0$ relation, i.e. equality mod finite.
Start with your favourite model, say $L$. Next add $\omega_1$ Cohen reals, and consider the permutations that modify each coordinate by "bit flipping" on finitely many natural numbers, independently on each coordinate. Finally, take the filter of subgroups given by countable support (i.e. on a countable set of coordinates we are guaranteed to not change anything).
It is now easy to show that in the symmetric extension:

*

*$\sf ZF$ holds, and for good measure so does $\sf DC$.

*The set of $E_0$-classes of the Cohen reals exists, i.e. $([r_\alpha]\mid\alpha<\omega_1)$, where $r_\alpha$ is the Cohen real.

*There is no choice function from that set. Therefore no choice function from $2^\omega/E_0$.

Doing something similar with Turing degrees is trickier, I'm guessing, since those are more complicated than just equivalence mod finite, but it's not unthinkable (I suppose something along the lines of bit flipping on a computable set might work, but I never really grokked Turing degrees to the level I can just throw it out there with certainty).
