Coding is hard

TL;DR

This paper reveals that the standard coding of compact metric spaces in second-order arithmetic significantly impacts the logical strength of theorems, making some as hard as full second-order arithmetic or countable choice.

Contribution

It demonstrates that the standard representation of compact metric spaces affects the logical strength of theorems, linking coding methods to foundational logical principles.

Findings

Certain theorems imply Feferman's projection principle

Formulations with representations are provable in weak fragments

Generalizations to higher-order arithmetic show similar results

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.