**TL;DR**: there are various definitions of the notion ‘countable set of reals’ and only one seems to lead to nice equivalences in Reverse Mathematics. In particular, injections and bijections to the naturals *à la Cantor* are not very suitable. A slightly more general notion leads to many equivalences involving regulated and bounded variation functions, as well as basic properties of the Riemann integral.**Long version**: Cantor’s pioneering work in set theory established that ‘infinity’ comes in different sizes, a fact that genuinely surprised even Karl Weierstrass. In particular, Cantor’s first set theory paper establishes that the real numbers are *not countable*. The latter notion can be made precise via a number of different definitions, as follows.

- A set is
*denumerable*if there is a sequence that includes all elements of . - A set is
*countable*if there is an injection to the naturals, i.e. there exists a mapping such that for al , we have . - A set is
*strongly countable*if there is a bijection to the naturals, i.e. there is an injection to the naturals that is also surjective: . - A set is
*height-countable*if there is a*height function*, i.e. a mapping such that for all , the set is finite.

The first three notions are well-known while height functions can be found here and there in the literature when discussing e.g. the countability of the rationals. Clearly, height-countability amounts to

*unions over of finite sets*

since we readily have in item 4. above.

As it happens, one readily shows that the reals are not denumerable in a weak system using Cantor’s diagonal argument (see Simpson’s excellent SOSOA, II.4.7). There is even an efficient algorithm that, given a sequence of reals, produces a real not in that sequence (see Gray, 1994).

By contrast, the following principles are surprisingly **hard** to prove in terms of comprehension.

**NIN** there is no injection from to .

**NBI** there is no bijection from to .

*Many* third-order theorems imply **NIN** and **NBI** while -in terms of comprehension- full second-order arithmetic comes to the fore in any proof of **NIN** or **NBI**; this hardness remains if we restrict to ‘nice’ function classes (see here). All relevant results can be found here in a joint paper with Dag Normann. We stress that **NIN** and **NBI** are the weakest known third-order principles that exhibit the aforementioned hardness.

In light of the previous paragraph, the uncountability of seems like a natural topic of study in Reverse Mathematics. *Try as we might, *we could not obtain any natural equivalences using injections or bijections to the naturals. By contrast, many equivalences may be found here for the following principle, over a conservative extension of ACA:

**NIN**: the unit interval is not height countable.

In particular, NIN is equivalent to the following:

1) For regulated , there is a point where is continuous (or quasi-continuous, or lower semi-continuous, or Darboux).

2) For regulated , the set of continuity points is dense in .

3) For regulated with Riemann integral , there is with (Bourbaki).

4) (Volterra) For regulated , there is such that and are both continuous or both discontinuous at .

5) (Volterra) For regulated , there is either where is discontinuous, or where is continuous.

6) For regulated , there is where is differentiable with derivative equal to .

7) For regulated , there are such that is infinite.

8) Blumberg’s theorem restricted to regulated functions.

Many more equivalences can be found in the associated paper, including equivalences for functions of bounded variation.

Finally, a fairly ‘weird’ fact is that the items 1-8 become provable (say in a conservative extension of ACA) if we add the additional condition ‘Baire 1’. There is no contradiction here as

*all regulated functions are Baire 1 on the unit interval* (*)

is of course provable in say ZF. Nonetheless, (*) is suprisingly hard to prove as (*) implies **NIN** (see here). We have no real explanation for this phenomenon.