Made with higher types
On the mathematical and foundational significance of the uncountable (arxiv link)
Dag Normann and Sam Sanders
The aim of this paper is to identify a number of basic theorems of uncountable mathematics that fall outside the Gödel hierarchy, and a fortiori outside the 'Big Five' of Reverse Mathematics. A list may be found below the following figure, in which we observe a side-branch for the medium range of the Gödel hierarchy.
Note that we use an inessential modification of the Gödel hierarchy: the higher-order systems with superscript 'omega' are conservative over the second-order systems for large formula classes.
The list of theorems similarly independent of the medium range is as follows.
-
Cousin lemma: an uncountable open cover of [0,1] has a finite sub-cover.
-
Lindelöf lemma: an uncountable open cover of R has a countable sub-cover.
-
Besicovitsch and Vitali covering lemmas.
-
Basic properties of the gauge integral, like uniqueness, Hake’s theorem,
and extension of the Riemann integral.
-
Neighbourhood Function Principle NFP from intuitionistic mathematics.
-
The existence of Lebesgue numbers for any uncountable open cover.
-
The Banach-Alaoglu theorem for any open cover.
-
The Heine-Young and Lusin-Young theorems, the tile theorem, and
the latter’s generalisation due to Rademacher.
We also study how e.g. the Turing jump functional interacts with the Cousin and Lindelöf lemmas, with surprising results.