Normann-Sanders 4

Uniformity in mathematics (arxiv link)

Dag Normann and Sam Sanders

The 19th century saw a systematic development of real analysis in which many theorems were proved using compactness. In the work of Dini, Pincherle, Bolzano, Young, Riesz, and Lebesgue, one finds such proofs which (sometimes with minor modification) additionally are highly uniform in the sense that the objects proved to exist only depend on few of the parameters of the theorem. More recently, similarly uniform results have been obtained as part of the redevelopment of analysis based on techniques from gauge inte- gration. Our aim is to study such ‘highly uniform’ theorems in Reverse Mathematics and computability theory. We identify a number of uniform theorems 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 HBU): 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.
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.

We also discuss the role of the axiom of choice in the previous. As a result, we show that the logical properties of the Lindelöf lemma are extremely dependent on the exact formulation (provable in second-order arithmetic versus not provable in ZF).