Can a subset of $\mathbb R$ of size $\aleph_1$ be explicitly constructed

axiom-of-choiceset-theory

The Continuum Hypothesis claims that $|\mathbb R|=\aleph_1$. This has already been proven unprovable within ZFC. However, we can prove within ZFC that $|\mathbb R|\ge\aleph_1$ and thus there exists $S\subset\mathbb R$ such that $|S| = \aleph_1$. Can such a set be explicitly constructed?

The most naive approach for this problem would consist in looking for a subset of $\mathbb R$ isomorphic to $\omega_1$, but one can easily show there is no such (because $\mathbb R$ contains a countable dense subset).

I understand some provable things within ZFC can not be explicitly constructed, e.g. propositions that require the axiom of choice, such as a good ordering for $\mathbb R$. Is this the case for such a set?

Best Answer

The basic strategy of an earlier answer of Asaf Karagila's can be used here too to show that there is no formula $\varphi$ which $\mathsf{ZFC}$ proves defines a set of reals of size $\aleph_1$. (Really, one proves: if $\mathsf{ZFC}\vdash\{x\in\mathbb{R}:\varphi(x)\}$ is uncountable then there is a forcing extension in which that set has size continuum.) The details are a bit technical, but I suspect this is folklore.

This, combined with the usual descriptive set theoretic obstacles (assuming $\neg\mathsf{CH}$ there is no Borel set of size $\aleph_1$, nor a projective set of size $\aleph_1$ if there are also large cardinals), gives a pretty strong negative answer.

Beyond this, you will need to make more precise your notion of "explicit construction."