{
  "id": "2409.04562",
  "version": "v1",
  "published": "2024-09-06T18:52:32.000Z",
  "updated": "2024-09-06T18:52:32.000Z",
  "title": "Coding is hard",
  "authors": [
    "Sam Sanders"
  ],
  "comment": "23 pages plus references",
  "categories": [
    "math.LO"
  ],
  "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.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2024-09-06T18:52:32.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03B30",
      "03F35"
    ],
    "keywords": [
      "countable choice",
      "coding compact metric spaces",
      "similar third-order statements",
      "full second-order arithmetic",
      "standard second-order representation"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 23,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}