{
  "id": "2007.07560",
  "version": "v1",
  "published": "2020-07-15T09:19:01.000Z",
  "updated": "2020-07-15T09:19:01.000Z",
  "title": "On the uncountability of $\\mathbb{R}$",
  "authors": [
    "Dag Normann",
    "Sam Sanders"
  ],
  "comment": "30 pages, 1 Figure, One Appendix",
  "categories": [
    "math.LO"
  ],
  "abstract": "Cantor's first set theory paper (1874) establishes the uncountability of $\\mathbb{R}$ based on the statement 'for any sequence of reals, there is another real different from all reals in the sequence'. The latter (in)famous result is well-studied and has been implemented as an efficient computer program. By contrast, the status of the uncountability of $\\mathbb{R}$ is not as well-studied, and we therefore study the logical and computational properties of $\\textsf{NIN}$ (resp. $\\textsf{NBI}$) the statement 'there is no injection (resp. bijection) from $[0,1]$ to $\\mathbb{N}$'. While intuitively weak, $\\textsf{NIN}$ (and similar for $\\textsf{NBI}$) is classified as rather strong on the `normal' scale, both in terms of which comprehension axioms prove $\\textsf{NIN}$ and which discontinuous functionals compute (Kleene S1-S9) the real numbers from $\\textsf{NIN}$. Indeed, full second-order arithmetic is essential in each case. To obtain a classification in which $\\textsf{NIN}$ and $\\textsf{NBI}$ are weak, we explore the `non-normal' scale based on (classically valid) continuity axioms and non-normal functionals, going back to Brouwer. In doing so, we derive $\\textsf{NIN}$ and $\\textsf{NBI}$ from basic theorems, like Arzel\\`a's convergence theorem for the Riemann integral (1885) and central theorems from Reverse Mathematics formulated with the standard definition of `countable set'. In this way, the uncountability of $\\mathbb{R}$ is a corollary to most basic mainstream mathematics; $\\textsf{NIN}$ and $\\textsf{NBI}$ are even (among) the weakest principles on the non-normal scale, which serendipitously reproves many of our previous results. Finally, $\\textsf{NIN}$ and $\\textsf{NBI}$ allow us to showcase to a wide audience the techniques (like Gandy selection) used in our ongoing project on the logical and computational properties of the uncountable.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2020-07-15T09:19:01.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03B30",
      "03F35",
      "03D55",
      "03D30"
    ],
    "keywords": [
      "uncountability",
      "cantors first set theory paper",
      "computational properties",
      "basic mainstream mathematics",
      "non-normal"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 30,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}