Continuum-many independent vectors over Q in R as a Q-vector space Let's put ourselves in the framework of ZF. Is it true that if we think of the set of real numbers as a rational vector space, there are continuum-many linearly independent vectors? I feel that we could then use this to make an injection from $\mathbb{R}$ to $\mathbb{R}/\mathbb{Q}$, the quotient vector space by the 1-dimensional subspace $\mathbb{Q}$. Does this strategy work? This is to help me think about the result that (in ZF) $|\mathbb{R}| \leq |\mathbb{R}/\mathbb{Q}|$, proved by Mycielski in 1964. I haven't looked at his paper, just trying to imagine how one would prove this result. 
 A: Let $f: 2^{\mathbb{N}} \rightarrow \mathbb{R}/\mathbb{Q}$ be the function given by
$$ f((a_i)_{i \in \mathbb{N}}) = \text{the equivalence class of }\sum_{k=0}^{\infty} \frac{b_k}{2^{(k+1)!}}$$
where $(b_i)_{i \in \mathbb{N}}=(a_0,a_0,a_1,a_0,a_1,a_2,\dots)$. Notice that a real number of the form $$\sum_{k=0}^{\infty} \frac{c_k}{2^{(k+1)!}}$$ where $(c_i)_{i \in \mathbb{N}} \in 2^{\mathbb{N}}$ is rational if and only if the sequence $(c_k)$ is eventually zero. Consequently, $f((a_i)_{i \in \mathbb{N}})=f((a'_i)_{i \in \mathbb{N}})$ if and only if the corresponding sequences $(b_i)_{i \in \mathbb{N}}$ and $(b'_i)_{i \in \mathbb{N}}$ are eventually equal if and only if $(a_i)_{i \in \mathbb{N}}=(a'_i)_{i \in \mathbb{N}}$. Finally, compose this function with your favorite explicit injection from $\mathbb{R}$ to $2^{\mathbb{N}}$. This gives you an injection from $\mathbb{R}$ to $\mathbb{R}/\mathbb{Q}$.
If you want to find a $\mathbb{Q}$-linearly independent subset of $\mathbb{R}$ of size continuum, consider the image of the map $g: \mathcal{A} \rightarrow \mathbb{R}$ given by
$$ g(S)=\displaystyle \sum_{k=0}^{\infty} \frac{\chi_{S}(k)}{2^{(k+1)!}}$$
where $\mathcal{A} \subseteq \mathcal{P}(\mathbb{N})$ is an almost disjoint family of size continuum. For example, enumerate the vertices of the full binary tree of height $\omega$ by $\mathbb{N}$ and let $\mathcal{A}$ be the set of (labels of) branches. To see why this set is linearly independent, see this nice answer of Tim Gowers on another MO question.
Note that both of these constructions can be done in ZF.
A: Yes. There are a few different ways to prove this. One that I like is based off the following construction of an injection from $\mathbb{R}$ to $\mathbb{R}/\mathbb{Q}$:
Let $\{q_i:i\in\mathbb{N}\}$ be an enumeration of the positive rationals; we can in ZF build a map $F$ from $2^{<\mathbb{N}}$ to $2^{<\mathbb{N}}$ such that:


*

*$F$ is monotonic: $\sigma\prec\tau\implies F(\sigma)\prec F(\tau)$.

*For each $i\in\mathbb{N}$, if $\sigma,\tau$ are distinct binary strings of length $i$, then there are no real numbers $a,b$ in $(0, 1)$ whose binary representations begin with $F(\sigma)$ and $F(\tau)$ respectively and which satisfy $a=bq$.
Now we observe:

$(*)\quad$For finite binary strings $\hat{\sigma},\hat{\tau}$ and rational $q$, there are proper extensions $\sigma',\tau'$ of $\hat{\sigma},\hat{\tau}$ respectively such that for all reals $c, d$ with binary expansions beginning with $\hat{\sigma},\hat{\tau}$ respectively, $c\not=qd$.

This is easy to prove, and since the finite binary strings are well-ordered we can pick such $\sigma',\tau'$ canonically. We now build $F$ recursively (and by the previous sentence this works in ZF alone): we set $F(\emptyset)=\emptyset$ and having defined $F(\sigma)$ for all $\sigma$ of length $<n$ we define $F(\rho)$ for $\rho$s of length $n+1$ by applying $(*)$ repeatedly, so that for any distinct $\rho_0,\rho_1$ of length $n+1$ satisfy: no reals $a, b$ in $(0, 1)$ with binary expansions beginning with $\rho_0,\rho_1$ respectively satisfy $a=qb$. 
But now distinct infinite binary sequences $g,h$, the reals $0.F(g)$ and $0.F(h)$ can't be rational multiples of each other. So the map $\mathcal{F}$ sending $g$ to $0.F(g)$ yields an injection of $2^\mathbb{N}$ into $\mathbb{R}/\mathbb{Q}$, and we then tweak it appropriately to get one from $\mathbb{R}$ into $\mathbb{R}/\mathbb{Q}$.

This basic kind of argument - break our goal into countably many "local" requirements, then organize them on the levels of a tree appropriately - is useful in a wide variety of situations, and is especially simple when the requirements are appropriately "continuous." For the problem here, what we need to do is fix an enumeration $\{\mathcal{L}_i: i\in\mathbb{N}\}$ of all the nontrivial linear combinations in finitely many variables - and while this is messier, no actual difficulties arise since we can always "break" a purported linear combination appropriately. (Another application I like is the construction of a closed set of size continuum which is an antichain under Turing reducibility.)
