Big in Reverse Mathematics: the uncountability of the real numbers

The uncountability of $\mathbb{R}$ is one of its most basic properties, known far outside of mathematics. Cantor's 1874 proof of the uncountability of $\mathbb{R}$ even appears in the very first paper on set theory, i.e. a historical milestone. In this paper, we study the uncountability of $\mathbb{R}$ in Kohlenbach's higher-order Reverse Mathematics (RM for short), in the guise of the following principle: $$\hbox{for a countable set $A\subset \mathbb{R}$, there exists $y\in \mathbb{R}\setminus A$.}$$ An important conceptual observation is that the usual definition of countable set -- based on injections or bijections to $\mathbb{N}$ -- does not seem suitable for the RM-study of mainstream mathematics; we also propose a suitable (equivalent over strong systems) alternative definition of countable set, namely union over $\mathbb{N}$ of finite sets; the latter is known from the literature and closer to how countable sets occur 'in the wild'. We identify a considerable number of theorems that are equivalent to the centred theorem based on our alternative definition. Perhaps surprisingly, our equivalent theorems involve most basic properties of the Riemann integral, regulated or bounded variation functions, Blumberg's theorem, and Volterra's early work circa 1881. Our equivalences are also robust, promoting the uncountability of $\mathbb{R}$ to the status of 'big' system in RM.