On the uncountability of $\mathbb{R}$

Dag Normann, Sam Sanders

Published 2020-07-15Version 1

Cantor's first set theory paper (1874) establishes the uncountability of $\mathbb{R}$ based on the statement 'for any sequence of reals, there is another real different from all reals in the sequence'. The latter (in)famous result is well-studied and has been implemented as an efficient computer program. By contrast, the status of the uncountability of $\mathbb{R}$ is not as well-studied, and we therefore study the logical and computational properties of $\textsf{NIN}$ (resp. $\textsf{NBI}$) the statement 'there is no injection (resp. bijection) from $[0,1]$ to $\mathbb{N}$'. While intuitively weak, $\textsf{NIN}$ (and similar for $\textsf{NBI}$) is classified as rather strong on the `normal' scale, both in terms of which comprehension axioms prove $\textsf{NIN}$ and which discontinuous functionals compute (Kleene S1-S9) the real numbers from $\textsf{NIN}$. Indeed, full second-order arithmetic is essential in each case. To obtain a classification in which $\textsf{NIN}$ and $\textsf{NBI}$ are weak, we explore the `non-normal' scale based on (classically valid) continuity axioms and non-normal functionals, going back to Brouwer. In doing so, we derive $\textsf{NIN}$ and $\textsf{NBI}$ from basic theorems, like Arzel\`a's convergence theorem for the Riemann integral (1885) and central theorems from Reverse Mathematics formulated with the standard definition of `countable set'. In this way, the uncountability of $\mathbb{R}$ is a corollary to most basic mainstream mathematics; $\textsf{NIN}$ and $\textsf{NBI}$ are even (among) the weakest principles on the non-normal scale, which serendipitously reproves many of our previous results. Finally, $\textsf{NIN}$ and $\textsf{NBI}$ allow us to showcase to a wide audience the techniques (like Gandy selection) used in our ongoing project on the logical and computational properties of the uncountable.