
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputability, Logic, AI Algorithms · Advanced Topology and Set Theory · Mathematical and Theoretical Analysis
