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 continuummany 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 1dimensional 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.

8$\begingroup$ This question seems related: Explicit big linearly independent sets. (At least to the first part of your post.) $\endgroup$ – Martin Sleziak Oct 6 '17 at 8:13

1$\begingroup$ Incidentally, Mycielski's 1964 paper Independent sets in topological algebras is mentioned in a comment to François G. Dorais' answer. So I suppose that this the same paper you mention in your post. $\endgroup$ – Martin Sleziak Oct 6 '17 at 8:23

$\begingroup$ @Burak this is a nice simple construction, please consider adding it as an answer. $\endgroup$ – David Roberts Oct 6 '17 at 11:33

$\begingroup$ @DavidRoberts: I deleted the comment and added it as an answer. Since the main question was something different, I had not considered posting it as an answer. $\endgroup$ – Burak Oct 6 '17 at 12:30

4$\begingroup$ Von Neumann in his paper Ein system algebraisch unabhangiger Zahlen, Math. Ann., 99(1928), 134141 had an explicit construction of continuum many algebraically indepepdent reals see the short description in TomkowiczWagon: The BanachTarski paradox, secon edition , p 95. $\endgroup$ – Péter Komjáth Oct 6 '17 at 16:29
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.

$\begingroup$ This answered my second question bypassing the first (I was typing on a phone and tried to avoid writing any maths, I will edit so it is clearer). Thanks for bumping this to an answer. $\endgroup$ – David Roberts Oct 6 '17 at 20:47

1$\begingroup$ @DavidRoberts: Since you seem to have accepted this answer, I edited the answer so that it now answers both of your questions separately. The second part is basically due to Tim Gowers, as linked in the answer, and the first part is inspired by this Wikipedia page. $\endgroup$ – Burak Oct 8 '17 at 19:39
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 wellordered 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.)