Reverse Mathematics of the uncountability of $\mathbb{R}$

Abstract

In his first set theory paper (1874), Cantor establishes the uncountability of $\mathbb{R}$. We study the latter in Kohlenbach's higher-order Reverse Mathematics, motivated by the observation that one cannot study concepts like `arbitrary mappings from $\mathbb{R}$ to $\mathbb{N}$' in second-order Reverse Mathematics. Now, it was recently shown that the following statement: $$ \text{ NIN: there is no injection from $[0,1]$ to $\mathbb{N}$,} $$ is hard to prove in terms of conventional comprehension. In this paper, we show that NIN is robust by establishing equivalences between NIN and NIN restricted to mainstream function classes, like: bounded variation, semi-continuity, and Borel. Thus, the aforementioned hardness of NIN is not due to the quantification over arbitrary $\mathbb{R}\rightarrow \mathbb{N}$-functions in NIN. Finally, we also study NBI, the restriction of NIN to bijections, and the connection to Cousin's lemma and Jordan's decomposition theorem.