The Biggest Five of Reverse Mathematics

TL;DR: Dag Normann and I have obtained LOTS of equivalences between the second-order Big Five of Reverse Mathematics and third-order theorems from mainstream analysis about (possibly) discontinuous functions, working in Kohlenbach’s higher-order Reverse Mathematics. We also show that slight generalisations or variations of the aforementioned third-order theorems fall FAR outside of the Big Five. Our paper is on the arxiv here.

The long version:

First of all, whatever one’s opinion on Reverse Mathematics (RM for short) even an ardent critic must admit is quite neat that there are four systems (WKL $_0$ , ACA $_0$ , ATR $_0$ , $\Pi_1^1$ -CA $_0$ ) which feature many equivalences to basic mathematical facts over the base theory RCA $_0$ . These five systems together are called the “Big Five” of RM.

Secondly, Dag and I have established (see here) a LOT more equivalences for the Big Five. We work in Kohlenbach’s higher-order RM, i.e. we assume the base theory RCA $_0^{\omega}$ . Over the latter (and slight extensions), one can prove an equivalence between second-order WKL $_0$ and the following third-order statements:

any third-order $[0,1] \rightarrow \mathbb{R}$ -function in $X$ , is bounded on $[0,1]$ ,

any bounded third-order $[0,1]\rightarrow \mathbb{R}$ -function in $Y$ has a supremum on $[0, 1]$ , (*)

any bounded third-order $[0,1] \rightarrow \mathbb{R}$ -function in $Z$ with a supremum, attains its maximum.

Here, $X, Y, Z$ are among well-known function classes based on: continuity, bounded variation, regulated, cadlag, Baire 1, upper or lower semicontinuity, quasi-continuity etc. A function class from logic we consider is ‘effectively Baire 2’, i.e. the double limit of a double sequence of continuous functions. Baire himself already noted that Baire 2 functions can be represented by effectively Baire 2 functions.

Similar results are possible for restrictions of the Cousin lemma to $X, Y, Z$ , where the latter is essentially the Heine-Borel theorem for uncountable coverings, as follows:

For any $\Psi:[0,1]\rightarrow \mathbb{R}^+$ , the uncountable covering $\cup_{x\in [0,1]} B(x, \Psi(x))$ has a finite sub-covering, i.e. there are $x_0, \dots, x_k \in [0,1]$ such that $\cup_{i\leq k} B(x_i, \Psi(x_i))$ covers the unit interval.

Similar results are possible for ACA $_0$ , ATR $_0$ , and $\Pi_1^1$ -CA $_0$ . In each case, one takes a second-order statement from analysis and introduces third-order generalisations or variations involving third-order function classes that contain (slightly) discontinuous functions. We also study the Jordan decomposition theorem and similar results on bounded variation and regulated functions.

In a nutshell, many many many equivalences are obtained between the second-order Big Five and third-order theorems, resulting in the Biggest Five to date. Similar results are possible for weak weak Koenig’s lemma and Vitali’s covering theorem.

Thirdly, slight generalisations and variations of the aforementioned third-order theorems are no longer in the RM of the Big Five, as shown by this example:

while (*) belongs to the RM of WKL $_0$ in case “ $Y$ = Baire 1” or $Y$ = quasi-continuity”, the principle (*) cannot be proved from the Big Five (and much stronger systems at the level of Z $_2$ ) in case “ $Y$ = Baire 2” or “ $Y$ = Baire 1*”.

Note that Baire 2 is a super-class of Baire 1, while Baire 1* is a sub-class. Moreover, the quasi-continuous functions form a huge class, as discussed in our paper, far beyond the Borel or measurable functions.

We have no explanation for the above phenomenon, but do point out it serves as a warning against coding: a truly huge difference between the supremum principle (*) for ‘Baire 2’ and ‘effectively Baire 2’ functions is identified. Indeed, for the latter class, RCA $_0^{\omega}+\Pi_1^1$ -CA $_0$ suffices for a proof, while for the former class, RCA $_0^{\omega}$ +Z $_2$ does not.

Finally, any comments are welcome, but please with an open mind regarding all things third-order!

2 thoughts on “The Biggest Five of Reverse Mathematics”

LukasHM says:
March 29, 2023 at 3:05 pm
Very interesting post! I find the idea of higher order reverse mathematics very natural but I have found it strangely difficult to find resources going over even basic aspects of it. For example, in Kohlenbach’s orginal paper he defines a higher order theory RCA0^omega that is conservative over RCA_0, but I haven’t been able to find similar higher order versions of the other Big Five. Do you know of any reference that defines a higher order version of, say, ACA0?
1. Sam Sanders says:
  May 8, 2023 at 5:31 pm
  Dag and I introduce a number of systems in the above paper (https://arxiv.org/abs/2212.00489), including higher-order counterparts of the Big Five. We also provide references, including to conservation results.

2 thoughts on “The Biggest Five of Reverse Mathematics”

Leave a Reply Cancel reply