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!