CODING IS HARD

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 $$ \begin{align*} {coding\ compact\ metric\ spaces\ in\ the\ language\ of\ second\text{-}order\ arithmetic\ can\ be\ as\ hard }\\ {as\ second\text{-}order\ arithmetic\ or\ countable\ choice}. \end{align*} $$ 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.