On two recent extensions of the Big Five of Reverse Mathematics

TL;DR

This paper explores two recent extensions of the Big Five framework in Reverse Mathematics within higher-order settings, identifying new equivalences and systems related to real analysis, uncountability, and measure theory.

Contribution

It introduces four new 'Big' systems and establishes numerous equivalences between second-order and third-order theorems in real analysis.

Findings

Many equivalences between second-order and third-order theorems in real analysis.

Identification of four new 'Big' systems related to uncountability and measure.

Connection to hyperarithmetical analysis enhances the theoretical framework.

Abstract

The program Reverse Mathematics in the foundations of mathematics seeks to identify the minimal axioms required to prove theorems of ordinary mathematics. One always assumes the base theory, a logical system embodying computable mathematics. As it turns out, many (most?) theorems are either provable in said base theory, or equivalent to one of four logical systems, collectively called the Big Five. This paper provides an overview of two recent extensions of the Big Five, working in Kohlenbach's higher-order framework. On one hand, we obtain a large number of equivalences between the second-order Big Five and third-order theorems of real analysis dealing with possibly discontinuous functions. On the other hand, we identify four new 'Big' systems, i.e. boasting many equivalences over the base theory, namely the uncountability of the reals, the Jordan decomposition theorem, the Baire category theorem, and Tao's pigeon hole principle for the Lebesgue measure. We discuss a connection to hyperarithmetical analysis, completing the picture.