编码是困难的
Coding is hard
AI总结：
本文证明在二阶算术中用标准表示编码紧度量空间会显著提升相关基本定理的逻辑强度，使其至少蕴含 Feferman 投影原理甚至完全二阶算术或可数选择，并建立了若干等价关系及高阶推广。
摘要：
数理逻辑的一个核心主题是根据逻辑强度在层级中对数学定理进行分类。理想情况下，一个定理在层级中的位置不应依赖于所使用的表示（又称编码）。在本文中，我们证明二阶算术中紧度量空间的标准表示具有深远的影响。为此，我们研究此类空间的基本定理，例如连续函数具有上确界以及可数集合具有零测度。我们证明这些以及类似的三阶命题至少蕴含 Feferman 的高度非构造性投影原理，在某些情况下甚至蕴含完全二阶算术或可数选择。当用表示（又称编码）来表述时，相关的二阶定理可以在相当弱的二阶算术片段中得到证明。因此，我们得出这样一个口号：用二阶算术语言对紧度量空间进行编码，其难度可能与二阶算术或可数选择本身一样高。我们相信每位数学家都应该了解这一口号，因为数学中的核心基础性论题都使用了紧度量空间的标准二阶表示。在为上述口号收集证据的过程中，我们建立了若干涉及 Feferman 投影原理与可数选择的等价关系。我们还研究了向四阶算术及更高阶的推广，得到了类似但更强的结果。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
