Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A note on continuous functions on metric spaces

Sam Sanders

TL;DR

The paper addresses how omitting second-order representations for metric spaces in Kohlenbach's higher-order Reverse Mathematics affects the provability of basic theorems about continuous functions on compact spaces. It shows that while some very specific third-order statements fall within the second-order Big Five, many natural variations escape those systems and require stronger axioms, highlighting a wild but not entirely unruly landscape for non-represented spaces. Central to the analysis are uncountability principles like $NIN_{[0,1]}$ and $NBI_{[0,1]}$, which arise from basic properties such as Heine–Borel compactness and are not provable in the base $Z_{2}^{\omega}$. The work connects coding choices to foundational outcomes, with implications for proof mining and the role of separability, and draws parallels to set-theoretic phenomena surrounding the continuum and choice principles.

Abstract

Continuous functions on the unit interval are relatively tame from the logical and computational point of view. A similar behaviour is exhibited by continuous functions on compact metric spaces equipped with a countable dense subset. It is then a natural question what happens if we omit the latter 'extra data', i.e. work with 'unrepresented' compact metric spaces. In this paper, we study basic third-order statements about continuous functions on such unrepresented compact metric spaces in Kohlenbach's higher-order Reverse Mathematics. We establish that some (very specific) statements are classified in the (second-order) Big Five of Reverse Mathematics, while most variations/generalisations are not provable from the latter, and much stronger systems. Thus, continuous functions on unrepresented metric spaces are 'wild', though 'more tame' than (slightly) discontinuous functions on the reals.

A note on continuous functions on metric spaces

TL;DR

The paper addresses how omitting second-order representations for metric spaces in Kohlenbach's higher-order Reverse Mathematics affects the provability of basic theorems about continuous functions on compact spaces. It shows that while some very specific third-order statements fall within the second-order Big Five, many natural variations escape those systems and require stronger axioms, highlighting a wild but not entirely unruly landscape for non-represented spaces. Central to the analysis are uncountability principles like and , which arise from basic properties such as Heine–Borel compactness and are not provable in the base . The work connects coding choices to foundational outcomes, with implications for proof mining and the role of separability, and draws parallels to set-theoretic phenomena surrounding the continuum and choice principles.

Abstract

Continuous functions on the unit interval are relatively tame from the logical and computational point of view. A similar behaviour is exhibited by continuous functions on compact metric spaces equipped with a countable dense subset. It is then a natural question what happens if we omit the latter 'extra data', i.e. work with 'unrepresented' compact metric spaces. In this paper, we study basic third-order statements about continuous functions on such unrepresented compact metric spaces in Kohlenbach's higher-order Reverse Mathematics. We establish that some (very specific) statements are classified in the (second-order) Big Five of Reverse Mathematics, while most variations/generalisations are not provable from the latter, and much stronger systems. Thus, continuous functions on unrepresented metric spaces are 'wild', though 'more tame' than (slightly) discontinuous functions on the reals.
Paper Structure (13 sections, 6 theorems, 15 equations)

This paper contains 13 sections, 6 theorems, 15 equations.

Table of Contents

  1. Introduction
  2. Motivation and background
  3. Introduction
  4. Higher-order Reverse Mathematics
  5. The coding practise of Reverse Mathematics
  6. Metric spaces and higher-order Reverse Mathematics
  7. Preliminaries and definitions
  8. Analysis on unrepresented metric spaces
  9. Obtaining the uncountability of the reals
  10. Variations on a theme
  11. Foundational musings
  12. Thoughts on coding
  13. Set theory and ordinary mathematics

Key Result

Theorem 1.1

The system $\textup{RCA}_{0}^{\omega}$ proves the following for $\mathbb{X}={\mathbb N}^{{\mathbb N}}$ or $\mathbb{X}={\mathbb R}$. The system $\textup{RCA}_{0}^{\omega}+\textup{WKL}_{0}$ proves the following for $\mathbb{X}=2^{{\mathbb N}}$ or $\mathbb{X}=[0,1]$.

Theorems & Definitions (15)

  • Theorem 1.1
  • proof
  • Definition 1.2
  • Definition 1.3
  • Definition 1.4: Compactness and around
  • Theorem 1.5
  • Remark 1.6: On excluded middle
  • Theorem 2.2: $\textup{RCA}_{0}^{\omega}+\textup{IND}_{1}$
  • proof
  • Theorem 2.3: $\textup{RCA}_{0}^{\omega}$
  • ...and 5 more