More than bargained for in Reverse Mathematics

TL;DR

This paper reveals that the Reverse Mathematics framework, through its coding of continuity, unintentionally introduces higher-order concepts, linking second-order and higher-order theorems and enriching the foundational understanding of continuity.

Contribution

It demonstrates that RM's coding of continuity leads to nonstandard and higher-order phenomena, bridging second-order and higher-order theorems in reverse mathematics.

Findings

RM-definition of continuity induces nonstandard continuity.

RM-theorems about continuity are implicitly higher-order.

Coding in RM introduces higher-type objects.

Abstract

Reverse Mathematics (RM for short) is a program in the foundations of mathematics with the aim of finding the minimal axioms required for proving theorems about countable and separable objects. RM usually takes place in second-order arithmetic and due to this choice of framework, continuous real-valued functions have to be represented by so-called codes. Kohlenbach has shown that the RM-definition of continuity-via-codes constitutes a slight constructive enrichment of the epsilon-delta definition, namely in the form of a modulus of continuity. In this paper, we show that the RM-definition of continuity also gives rise to a `nonstandard' enrichment in the form of nonstandard continuity from Nonstandard Analysis. This observation allows us to (i) establish that RM-theorems related to continuity are implicitly higher-order statements, (ii) prove equivalences between RM-theorems concerning continuity and their associated higher-order versions, and (iii) obtain explicit equivalences between higher-order theorems from the equivalence between the corresponding RM-theorems. Moreover, we show that it is exactly the RM-definition of continuity-via-codes which gives rise to these higher-order phenomena. In conclusion, we establish that the practice of coding in RM, designed to obviate higher-type objects, actually introduces a host of new ones.