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

TL;DR

This paper explores the uncountability of the real numbers within higher-order Reverse Mathematics, demonstrating the robustness of the uncountability principle across various function classes and connecting it to classical theorems.

Contribution

It establishes equivalences of the uncountability principle with its restrictions to common function classes, showing its inherent complexity beyond arbitrary functions.

Findings

NIN is equivalent to its restriction to bounded variation functions.

NIN's hardness is not due to quantification over arbitrary functions.

Connections between NIN, Cousin's lemma, and Jordan's decomposition are established.

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.