On the Uncountability Of

Journal of Symbolic Logic 87 (4):1474-1521 (2022)
  Copy   BIBTEX


Cantor’s first set theory paper (1874) establishes the uncountability of ${\mathbb R}$. We study this most basic mathematical fact formulated in the language of higher-order arithmetic. In particular, we investigate the logical and computational properties of ${\mathsf {NIN}}$ (resp. ${\mathsf {NBI}}$ ), i.e., the third-order statement there is no injection resp. bijection from $[0,1]$ to ${\mathbb N}$. Working in Kohlenbach’s higher-order Reverse Mathematics, we show that ${\mathsf {NIN}}$ and ${\mathsf {NBI}}$ are hard to prove in terms of (conventional) comprehension axioms, while many basic theorems, like Arzelà’s convergence theorem for the Riemann integral (1885), are shown to imply ${\mathsf {NIN}}$ and/or ${\mathsf {NBI}}$. Working in Kleene’s higher-order computability theory based on S1–S9, we show that the following fourth-order process based on ${\mathsf {NIN}}$ is similarly hard to compute: for a given $[0,1]\rightarrow {\mathbb N}$ -function, find reals in the unit interval that map to the same natural number.



    Upload a copy of this work     Papers currently archived: 78,059

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Existence and Strong Uncountability.Jonah P. B. Goldwater - 2017 - Acta Analytica 32 (3):321-331.
Cantor theorem and friends, in logical form.Silvio Valentini - 2013 - Annals of Pure and Applied Logic 164 (4):502-508.
Conceptions of Infinity and Set in Lorenzen’s Operationist System.Carolin Antos - 2021 - In Gerhard Heinzmann & Gereon Wolters (eds.), Paul Lorenzen -- Mathematician and Logician. Springer Verlag. pp. 23-46.


Added to PP

8 (#998,320)

6 months
1 (#486,551)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Dag Normann
University of Oslo
Sam Sanders
Ruhr-Universität Bochum

Citations of this work

Add more citations

References found in this work

No references found.

Add more references