Where can I find a proof of ($\aleph_1 \leq 2^{\aleph_0}$ is independent of ZF)?

Question

In "A tutorial on countable ordinals" [1], in page 25, Forster uses the fact that $\aleph_1 \leq 2^{\aleph_0}$ is independent of ZF to prove that there is no definable family of fundamental sequences up to $\omega_1$. I know the proof must be technical, and I can't find anywhere a proof of that. Does anyone know of any book or paper that proves it? Thanks!

[1] https://www.dpmms.cam.ac.uk/~tf/fundamentalsequence.pdf

Answer 1

The easiest places to find this consistency proof are the following papers:

1. Solovay, R. M., A model of set-theory in which every set of reals is Lebesgue measurable, Ann. Math. (2) 92, 1-56 (1970). ZBL0207.00905.

2. Truss, John, Models of set theory containing many perfect sets, Ann. Math. Logic 7, 197-219 (1974). ZBL0302.02024.

Some remarks:

1. If $\aleph_1\nleq2^{\aleph_0}$, then there is no real number $x$ such that $L[x]$ computes $\omega_1$ correctly. Therefore $\omega_1$ is a limit cardinal in $L$.

2. If you assume countable choice holds for sets of real numbers, then $\omega_1$ is regular, and by the above, it is inaccessible in $L$. If you don't mind $\omega_1$ being singular, then you can do just fine without assuming large cardinals.

3. The famous Feferman–Levy model is another example of this situation. In that model $\Bbb R$ is a countable union of countable sets. I think the original paper was only published as a notice in Notices of the AMS, but you can find modern presentations in Jech's books as well as numerous masters and doctoral theses over the year (e.g. Ioanna M. Dimitriou's theses both present the construction as an example of a symmetric extension).

Note that in any case, some use of forcing and symmetries is necessary. Depending on your set theoretic background, this might be a simple read (Solovay's paper is very readable), or an uphill battle.