Sanders-RM of topology

Reverse Mathematics of topology: dimension, paracompactness, and splittings (arxiv link)

Sam Sanders

As suggested by the title, this paper deals with the study of the topological notions of dimension and paracompactness in Reverse Mathematics. As to splittings, there are some examples in Reverse Mathematics of theorems A, B, C such that A ↔ (B ∧ C), i.e. A can be split into two independent (fairly natural) parts B and C; the aforementioned topological notions give rise to a number of splittings involving natural A, B, C. We identify a number of basic theorems from topology that fall outside the Gödel hierarchy, and a fortiori outside the 'Big Five' of Reverse Mathematics. A list, including previous results, 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 (aka HBT): an uncountable open cover of [0,1] has a finite sub-cover.
Lindelöf lemma (aka LIL): 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.
Uniform theorems like uniform Pincherele's theorem and uniform Heine's theorem. The latter expresses that a continuous f on [0,1] has a modulus of uniform continuity, and the latter only depends on a modulus of continuity for f.
The paracompactness of the unit interval (or the real line).
The Urysohn 'dimension; identity for the unit interval (or the real line)
The existence of partitions of unity for the unit interval (or the real line)

We also show that covering lemmas like HBT and LIL have a certain robustness, in that they do not depend on the exact definition of cover, even in the absence of the axiom of choice.