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, ACA, ATR, -CA) which feature **many** equivalences to basic mathematical facts over the base theory RCA. 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. Over the latter (and slight extensions), one can prove an equivalence between **second-order** WKL and the following **third-order** statements:

*any third-order -function in , is bounded on *,

*any bounded third-order -function in has a supremum on *, (*)

*any bounded third-order -function in with a supremum, attains its maximum*.

Here, 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 , where the latter is essentially the Heine-Borel theorem for uncountable coverings, as follows:

*For any , the uncountable covering has a finite sub-covering, i.e. there are such that covers the unit interval. *

Similar results are possible for ACA, ATR, and -CA. 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 in case “ = Baire 1” or = quasi-continuity”, the principle (*) cannot be proved from the Big Five (and much stronger systems at the level of Z) in case “ = Baire 2” or “ = 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-CA suffices for a proof, while for the former class, RCA+Z does not.

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

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?

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.