Skip to content

The Proof Theory Blog

PA ⊢ ∀x ∃y A(x,y) ⇒ ∃t . T ⊢ ∀x A(x,t(x))

Menu
  • Home
  • About
  • Contribute
  • Resources
Menu

The Biggest Five of Reverse Mathematics

Posted on January 12, 2023January 12, 2023 by Sam Sanders

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!

Leave a Reply Cancel reply

Your email address will not be published. Required fields are marked *

Meta

  • Register
  • Log in
  • Entries RSS
  • Privacy Policy

Search

© 2023 The Proof Theory Blog | Powered by Minimalist Blog WordPress Theme
The Proof Theory Blog uses cookies, but you can opt-out if you wish. For further information see our privacy policy. Cookie settingsAccept
Privacy & Cookies Policy

Privacy Overview

This website uses cookies to improve your experience while you navigate through the website. Out of these cookies, the cookies that are categorized as necessary are stored on your browser as they are essential for the working of basic functionalities of the website. We also use third-party cookies that help us analyze and understand how you use this website. These cookies will be stored in your browser only with your consent. You also have the option to opt-out of these cookies. But opting out of some of these cookies may have an effect on your browsing experience.
Necessary
Always Enabled
Necessary cookies are absolutely essential for the website to function properly. This category only includes cookies that ensures basic functionalities and security features of the website. These cookies do not store any personal information.
Non-necessary
Any cookies that may not be particularly necessary for the website to function and is used specifically to collect user personal data via analytics, ads, other embedded contents are termed as non-necessary cookies. It is mandatory to procure user consent prior to running these cookies on your website.
SAVE & ACCEPT