Does the existence of this quotient set depend on the Axiom of Choice?

Question

We know the familiar equivalent relation on $\mathbb{R}$, which is $$ x\sim y\Leftrightarrow x-y\in\mathbb{Q} $$

After quoting this relation, we have the quotient set $$ \mathbb{R}/_\sim = \{x + \mathbb{Q} : x\in\mathbb{R}\} $$

I know that if we want to construct a set of representative elements of the above relation, we need the Axiom of Choice. So if I write $$ \mathbb{R}/_\sim = \{[x] : x\in\mathbb{R}\text{ are representatives}\} $$

I need AC. But my question is, does existence of $\mathbb{R}/_\sim$ in the first formula need the axiom?

To my understanding, the existence of quotient set has nothing to do with the Axiom of Choice.

Answer 1

You don't need choice for the existence of $\mathbb{R}/{\sim}$, but you do need choice to assert that there is a set of $\sim$-class representatives.

To demonstrate this: we can say $$\mathbb{R}/{\sim} = \{ A \in \mathcal{P}(\mathbb{R}) \, :\, (\forall y,z \in A)(\forall q \in \mathbb{Q})(y-z \in \mathbb{Q} \wedge y+q \in A) \} \setminus \{ \varnothing \}$$ This can be proved to exist inside $\mathsf{ZF}$, because we can define $\mathbb{Q}, \mathbb{R}, \mathcal{P}(\mathbb{R}), +, -, \setminus, \varnothing$ in $\mathsf{ZF}$ and then apply Separation.

But a set of coset representatives is precisely (the image of) a choice function for $\mathbb{R}/{\sim}$, the existence of which does require the axiom of choice.

Answer 2

The quotient exists just fine.

Consider the map $x\mapsto\{x+q\mid q\in\Bbb Q\}$ as a function from $\Bbb R$ into $\mathcal P(\Bbb R)$. This function is perfectly definable without the axiom of choice. In fact we just defined it. And by the axiom of replacement we know that the image of a set under a definable function is a set.

And what is the image? It is exactly $\Bbb R/\sim$.