The Biggest Five of Reverse Mathematics

[Sam Sanders]

Dear FOM,

here are some musing for the New Year about a favourite topic, namely reverse mathematics.  


First of all, whatever one’s opinion on reverse mathematics, even an ardent critic must admit is quite neat that there are 
four systems (WKL_0, ACA_0, ATR_0, Pi11-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”.  


Secondly, the Big Five have gotten a LOT bigger in 2022!  Let us work in Kohlenbach’s ‘higher-order’ reverse mathematics, 
i.e. we assume the base theory RCA_0^omega.  Over the latter (and mild extensions), one can prove an equivalence between 
*second-order* WKL_0  and the following *third-order* statements:

“any third-order [0,1] -> R -function in X, is bounded on [0,1]”

“any bounded third-order [0,1]-> R-function in Y has a supremum on [0, 1]” (*)

“any bounded third-order [0,1]-> 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…

Similar variations are possible for the Cousin lemma (which is essentially the Heine-Borel theorem for uncountable coverings).
Similar results are possible for ACA_0, ATR_0, and Pi11-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.  

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.  


Thirdly, slight generalisations AND variations of the aforementioned third-order theorems are no longer in the RM of the Big Five:    

while (*) belongs to the RM of WKL_0 in case “Y = Baire 1”,
the principle (*) cannot be proved from the Big Five (and much 
stronger systems) in case “Y=Baire 2” or “Y=Baire 1*”  

Note that Baire 2 is a superclass of Baire 1, while Baire 1* is a sub-class.  

We have no explanation of this phenomenon but do mention it as a “caution against coding”
in second-order arithmetic: how would one obtain such results using the known second-order codes?


Finally, the interested reader will consult the following paper:

https://arxiv.org/abs/2212.00489

where they can find (too) many examples of the above “Biggest Five” equivalences.  


Best,

Sam