Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Coding is hard

Sam Sanders

TL;DR

The paper investigates how coding compact metric spaces in the language of second-order arithmetic affects foundational strength in higher-order Reverse Mathematics. It shows that several natural third-order statements about compact metric spaces (such as separability, countable-measure-zero sets, and supremum principles for continuous functions) logically imply strong axioms, including Feferman's projection principle $\textup{Proj}_{1}$ (and, in some cases, full ${\textsf{Z}}_{2}$ or countable choice) when formulated without codes. Conversely, when these statements are formulated with codes, their second-order consequences lie in relatively weak fragments (e.g., $\textup{ACA}_{0}^{\omega}$), illustrating a pronounced coding gap. The authors develop robust equivalences such as $\textup{BOOT}$ being equivalent to $\textup{RANGE}$ and provide templates that generalize to fourth-order and higher-order arithmetic. The results emphasize the significant impact of representation schemes on the logical strength of foundational theorems and suggest broader implications for computable analysis and Reverse Mathematics.

Abstract

A central topic in mathematical logic is the classification of theorems from mathematics in hierarchies according to their logical strength. Ideally, the place of a theorem in a hierarchy does not depend on the representation (aka coding) used. In this paper, we show that the standard representation of compact metric spaces in second-order arithmetic has a profound effect. To this end, we study basic theorems for such spaces like a continuous function has a supremum and a countable set has measure zero. We show that these and similar third-order statements imply at least Feferman's highly non-constructive projection principle, and even full second-order arithmetic or countable choice in some cases. When formulated with representations (aka codes), the associated second-order theorems are provable in rather weak fragments of second-order arithmetic. Thus, we arrive at the slogan that coding compact metric spaces in the language of second-order arithmetic can be as hard as second-order arithmetic or countable choice. We believe every mathematician should be aware of this slogan, as central foundational topics in mathematics make use of the standard second-order representation of compact metric spaces. In the process of collecting evidence for the above slogan, we establish a number of equivalences involving Feferman's projection principle and countable choice. We also study generalisations to fourth-order arithmetic and beyond with similar-but-stronger results.

Coding is hard

TL;DR

The paper investigates how coding compact metric spaces in the language of second-order arithmetic affects foundational strength in higher-order Reverse Mathematics. It shows that several natural third-order statements about compact metric spaces (such as separability, countable-measure-zero sets, and supremum principles for continuous functions) logically imply strong axioms, including Feferman's projection principle (and, in some cases, full or countable choice) when formulated without codes. Conversely, when these statements are formulated with codes, their second-order consequences lie in relatively weak fragments (e.g., ), illustrating a pronounced coding gap. The authors develop robust equivalences such as being equivalent to and provide templates that generalize to fourth-order and higher-order arithmetic. The results emphasize the significant impact of representation schemes on the logical strength of foundational theorems and suggest broader implications for computable analysis and Reverse Mathematics.

Abstract

A central topic in mathematical logic is the classification of theorems from mathematics in hierarchies according to their logical strength. Ideally, the place of a theorem in a hierarchy does not depend on the representation (aka coding) used. In this paper, we show that the standard representation of compact metric spaces in second-order arithmetic has a profound effect. To this end, we study basic theorems for such spaces like a continuous function has a supremum and a countable set has measure zero. We show that these and similar third-order statements imply at least Feferman's highly non-constructive projection principle, and even full second-order arithmetic or countable choice in some cases. When formulated with representations (aka codes), the associated second-order theorems are provable in rather weak fragments of second-order arithmetic. Thus, we arrive at the slogan that coding compact metric spaces in the language of second-order arithmetic can be as hard as second-order arithmetic or countable choice. We believe every mathematician should be aware of this slogan, as central foundational topics in mathematics make use of the standard second-order representation of compact metric spaces. In the process of collecting evidence for the above slogan, we establish a number of equivalences involving Feferman's projection principle and countable choice. We also study generalisations to fourth-order arithmetic and beyond with similar-but-stronger results.
Paper Structure (13 sections, 7 theorems, 17 equations)

This paper contains 13 sections, 7 theorems, 17 equations.

Table of Contents

  1. Introduction and preliminaries
  2. Aim
  3. Introduction
  4. Preliminaries
  5. Metric spaces in higher-order order arithmetic
  6. Some axioms of higher-order arithmetic
  7. Main results
  8. Introduction
  9. Metric spaces and separability
  10. Countable and measure zero sets in metric spaces
  11. Continuous functions on metric spaces
  12. Introduction
  13. The supremum as a sequence

Key Result

Theorem 2.2

The following statement implies $\textup{BOOT}$ and $\textup{QF-AC}^{0,1}$. We can replace 'sequential' by 'limit point' or 'countable' or 'open cover'.

Theorems & Definitions (18)

  • Definition 1.1
  • Definition 1.2: Compactness and around
  • Remark 2.1: On the law of excluded middle
  • Theorem 2.2: $\textup{ACA}_{0}^{\omega}+\Sigma\textup{-IND}$
  • proof
  • Corollary 2.3: $\textup{ACA}_{0}^{\omega}+\Sigma\textup{-IND}$
  • proof
  • Theorem 2.4: $\textup{ACA}_{0}^{\omega}$
  • proof
  • Definition 2.5
  • ...and 8 more