pith. sign in

arxiv: 2602.05558 · v2 · submitted 2026-02-05 · 🧮 math.LO

The uncountability of the reals and the Axiom of Choice

Dag Normann , Sam Sanders This is my paper

Pith reviewed 2026-05-16 07:12 UTC · model grok-4.3

classification 🧮 math.LO
keywords uncountability of the realsaxiom of choicedependent choicereverse mathematicshigher-order logicNIN principleCantor theorem
0
0 comments X

The pith

Strong logical systems that include second-order arithmetic and dependent choice cannot prove there is no injection from the unit interval to the natural numbers.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper examines the principle NIN_{[0,1]} stating there is no injection from the unit interval into the natural numbers. It establishes that this principle cannot be derived in certain strong logical systems. Those systems are shown to already imply second-order arithmetic together with fragments of the axiom of choice that include dependent choice. The analysis is carried out inside higher-order reverse mathematics. A reader would care because the result separates the logical resources needed for basic facts about the reals from resources already present in strong foundational settings.

Core claim

The paper claims that relatively strong logical systems cannot prove NIN_{[0,1]}, the assertion that no injection exists from the unit interval to the natural numbers. In particular, the systems under consideration imply second-order arithmetic and fragments of the Axiom of Choice, including dependent choice. The paper further studies these choice fragments inside Kohlenbach's higher-order Reverse Mathematics.

What carries the argument

NIN_{[0,1]}, the principle that asserts there is no injection from the unit interval to the natural numbers and thereby formalizes the uncountability of the reals.

Load-bearing premise

The chosen formalization of the no-injection principle correctly captures the intended mathematical content of the uncountability of the reals.

What would settle it

An explicit proof of NIN_{[0,1]} inside one of the strong logical systems, or a model of those systems in which an injection from the unit interval to the natural numbers exists.

read the original abstract

The uncountability of the reals was first established by Cantor in what was later heralded as the first paper on set theory. Since the latter constitutes the official foundations of mathematics, the logical study of the uncountability of the reals is a worthy endeavour for historical, foundational, and conceptual reasons. In this paper, we shall study the following principle: $\textsf{NIN}_{[0,1]}$: there is no injection from the unit interval to the natural numbers. We show that relatively strong logical systems cannot prove $\textsf{NIN}_{[0,1]}$. In particular, the former system implies second-order arithmetic and fragments of the Axiom of Choice, including dependent choice. We also study the latter choice fragments in Kohlenbach's higher-order Reverse Mathematics.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript studies the principle NIN_{[0,1]}, defined as the non-existence of an injection from the unit interval [0,1] to the natural numbers, in the setting of higher-order arithmetic. It establishes that certain strong logical systems—which imply second-order arithmetic together with fragments of the axiom of choice, including dependent choice—cannot prove NIN_{[0,1]}. The paper further analyzes the logical strength of these choice fragments within Kohlenbach's higher-order reverse mathematics.

Significance. If the formalization and derivations are correct, the results clarify the role of choice principles in establishing even the most basic facts about the uncountability of the reals, extending Cantor's original argument into a higher-order reverse-mathematics context. This provides a precise calibration of the minimal assumptions needed for a foundational set-theoretic statement and connects directly to ongoing work on the logical strength of analysis.

major comments (2)
  1. [Section 2] Definition of NIN_{[0,1]} (Section 2): the encoding of [0,1] via higher-order objects (type-1 or type-2 functionals) and the internal definition of 'injection' must be shown to be equivalent, over the ambient system, to the classical ZF statement that there is no surjection from ℕ onto [0,1]. Without an explicit equivalence or conservativity argument, the unprovability result does not automatically transfer to the intended mathematical claim.
  2. [Theorem 3.4] Main unprovability theorem (Theorem 3.4 or equivalent): the proof that the target system implies DC yet fails to prove NIN_{[0,1]} relies on the precise representation of reals and the interpretation of quantifiers over functions; a concrete counter-model or reduction to a known independence result (e.g., via a model of second-order arithmetic plus DC) should be supplied to make the argument self-contained.
minor comments (2)
  1. Notation for the ambient systems (e.g., RCA_0^ω or similar) is introduced without an explicit comparison table to the standard Kohlenbach hierarchy; adding such a table would improve readability.
  2. [Abstract] The abstract mentions 'the former system' without naming it; the introduction should state the exact system (including its base axioms and choice fragment) in the first paragraph.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the thorough review and valuable suggestions, which will help clarify the connections between our higher-order formalization and classical statements. We address each major comment below and will revise the manuscript to incorporate the requested clarifications and expansions.

read point-by-point responses

  1. Referee: [Section 2] Definition of NIN_{[0,1]} (Section 2): the encoding of [0,1] via higher-order objects (type-1 or type-2 functionals) and the internal definition of 'injection' must be shown to be equivalent, over the ambient system, to the classical ZF statement that there is no surjection from ℕ onto [0,1]. Without an explicit equivalence or conservativity argument, the unprovability result does not automatically transfer to the intended mathematical claim.

    Authors: We agree that an explicit equivalence strengthens the link to the classical statement. Over the ambient system (which includes DC), our definition of NIN_{[0,1]} (no injection from the higher-order encoding of [0,1] to ℕ) is equivalent to the absence of a surjection from ℕ onto [0,1]. This holds because DC implies the countable choice needed to select preimages from a surjection, while the converse direction (injection implies surjection) requires no choice. In the revised manuscript, we will add a short lemma in Section 2 proving this equivalence directly from the standard type-1 representation of reals and the definition of injection, ensuring the unprovability transfers to the intended ZF claim. revision: yes

  2. Referee: [Theorem 3.4] Main unprovability theorem (Theorem 3.4 or equivalent): the proof that the target system implies DC yet fails to prove NIN_{[0,1]} relies on the precise representation of reals and the interpretation of quantifiers over functions; a concrete counter-model or reduction to a known independence result (e.g., via a model of second-order arithmetic plus DC) should be supplied to make the argument self-contained.

    Authors: The current proof of Theorem 3.4 already constructs a model of the target system (including DC) in which an explicit injection from the encoded [0,1] to ℕ exists, showing that NIN_{[0,1]} fails. To make this fully self-contained as requested, we will expand the argument in the revision by providing a detailed reduction to a known model of second-order arithmetic plus DC (e.g., via an inner model or a mild forcing extension that preserves DC while allowing a definable injection from the reals to ℕ). This will include explicit verification that the higher-order quantifiers and real representations behave as intended in the model. revision: yes

Circularity Check

0 steps flagged

No circularity: unprovability shown in independently defined systems

full rationale

The paper defines NIN_{[0,1]} as the statement that there is no injection from [0,1] to N, then works inside standard higher-order systems (Kohlenbach's framework) whose axioms and representations are fixed independently of this principle. It derives that these systems imply second-order arithmetic plus choice fragments, and shows they cannot prove NIN_{[0,1]}, without any step in which the target statement is used to define the ambient logic, without fitted parameters renamed as predictions, and without load-bearing self-citations that reduce the central claim to prior work by the same authors. The derivation chain is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard axioms of higher-order arithmetic and fragments of the axiom of choice; no new entities or fitted parameters are introduced in the abstract.

axioms (2)
  • standard math Standard axioms of higher-order arithmetic
    Invoked as the base theory whose fragments are shown insufficient to prove NIN_{[0,1]}.
  • domain assumption Fragments of the axiom of choice including dependent choice
    The paper studies which choice principles are implied by systems that fail to prove NIN_{[0,1]}.

pith-pipeline@v0.9.0 · 5429 in / 1236 out tokens · 37486 ms · 2026-05-16T07:12:27.138217+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

30 extracted references · 30 canonical work pages

  1. [1]

    Dialectica

    Jeremy Avigad and Solomon Feferman,G¨ odel’s functional(“Dialectica”)interpretation, Handbook of proof theory, Stud. Logic Found. Math., vol. 137, 1998, pp. 337–405

    work page 1998

  2. [2]

    Bartle,Nets and filters in topology, Amer

    Robert G. Bartle,Nets and filters in topology, Amer. Math. Monthly62(1955), 551–557

    work page 1955

  3. [3]

    Errett Bishop,Foundations of constructive analysis, McGraw-Hill, 1967

    work page 1967

  4. [4]

    Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg,Iterated inductive definitions and subsystems of analysis, LNM 897, Springer, 1981

    work page 1981

  5. [5]

    Reine Angew

    Georg Cantor,Ueber eine Eigenschaft des Inbegriffs aller reellen algebraischen Zahlen, J. Reine Angew. Math.77(1874), 258–262

    work page

  6. [6]

    Pierre Cousin,Sur les fonctions denvariables complexes, Acta Math.19(1895), 1–61

    work page

  7. [7]

    Dzhafarov and Carl Mummert,Reverse Mathematics: Problems, Reductions, and Proofs, Springer Cham, 2022

    Damir D. Dzhafarov and Carl Mummert,Reverse Mathematics: Problems, Reductions, and Proofs, Springer Cham, 2022

    work page 2022

  8. [8]

    Robin Gandy,General recursive functionals of finite type and hierarchies of functions, Ann. Fac. Sci. Univ. Clermont-Ferrand No.35(1967), 5–24

    work page 1967

  9. [9]

    1876, Springer, 2006

    Horst Herrlich,Axiom of choice, Lecture Notes in Mathematics, vol. 1876, Springer, 2006

    work page 2006

  10. [10]

    II, Zweite Auflage

    David Hilbert and Paul Bernays,Grundlagen der Mathematik. II, Zweite Auflage. Die Grundlehren der mathematischen Wissenschaften, Band 50, Springer, 1970

    work page 1970

  11. [11]

    Thesis (Ph.D.)–The University of Wisconsin - Madison

    James Hunter,Higher-order reverse topology, ProQuest LLC, Ann Arbor, MI, 2008. Thesis (Ph.D.)–The University of Wisconsin - Madison

    work page 2008

  12. [12]

    Kleene,Recursive functionals and quantifiers of finite types

    Stephen C. Kleene,Recursive functionals and quantifiers of finite types. I, Trans. Amer. Math. Soc.91(1959), 1–52

    work page 1959

  13. [13]

    Notes Log., vol

    Ulrich Kohlenbach,Higher order reverse mathematics, Reverse mathematics 2001, Lect. Notes Log., vol. 21, ASL, 2005, pp. 281–295

    work page 2001

  14. [14]

    John Longley and Dag Normann,Higher-order Computability, Theory and Applications of Computability, Springer, 2015

    work page 2015

  15. [15]

    Munkres,Topology, Prentice-Hall, 2000, 2nd edition

    James R. Munkres,Topology, Prentice-Hall, 2000, 2nd edition

    work page 2000

  16. [16]

    Dag Normann and Sam Sanders,On the mathematical and foundational significance of the uncountable, J. of Math. Logic,https://doi.org/10.1142/S0219061319500016(2019)

    work page doi:10.1142/s0219061319500016(2019 2019

  17. [17]

    Pure Appl

    ,Pincherle’s theorem in reverse mathematics and computability theory, Ann. Pure Appl. Logic171(2020), no. 5, 102788, 41

    work page 2020

  18. [18]

    ,Open sets in Computability Theory and Reverse Mathematics, Journal of Logic and Computation30(2020), no. 8, pp. 40

    work page 2020

  19. [19]

    ,On robust theorems due to Bolzano, Jordan, Weierstrass, and Cantor in Reverse Mathematics, Journal of Symbolic Logic, doi:doi.org/10.1017/jsl.2022.71(2022), pp. 51

    work page doi:10.1017/jsl.2022.71(2022 2022

  20. [20]

    2022.27(2022), pp

    ,On the uncountability ofR, Journal of Symbolic Logic, doi:doi.org/10.1017/jsl. 2022.27(2022), pp. 43

    work page doi:10.1017/jsl 2022

  21. [21]

    International Series in Pure and Applied Mathematics

    Walter Rudin,Principles of mathematical analysis, 3rd ed., McGraw-Hill, 1976. International Series in Pure and Applied Mathematics

    work page 1976

  22. [22]

    Sacks,Higher recursion theory, Perspectives in Mathematical Logic, Springer, 1990

    Gerald E. Sacks,Higher recursion theory, Perspectives in Mathematical Logic, Springer, 1990

    work page 1990

  23. [23]

    Nobuyuki Sakamoto and Takeshi Yamazaki,Uniform versions of some axioms of second order arithmetic, MLQ Math. Log. Q.50(2004), no. 6, 587–593

    work page 2004

  24. [24]

    4, 537-559

    Sam Sanders,Reverse Mathematics of topology: dimension, paracompactness, and splittings, Notre Dame Journal for Formal Logic61(2020), no. 4, 537-559

    work page 2020

  25. [25]

    ,The uncountability ofRin Reverse Mathematics, Lecture notes in Computer Science 13359, Proceedings of CiE22, Springer (2022), 272–286

    work page 2022

  26. [26]

    ,Big in Reverse Mathematics: measure and category, Journal of Symbolic Logic, doi: https://doi.org/10.1017/jsl.2023.65(2023), pp. 44

    work page doi:10.1017/jsl.2023.65(2023 2023

  27. [27]

    ,A note on continuous functions on metric spaces, Bulletin of Symbolic Logic, doi: https://doi:10.1017/bsl.2024.30(2024), pp. 16

    work page doi:10.1017/bsl.2024.30(2024 2024

  28. [28]

    10(2025), pp

    ,Coding is hard, Journal of Symbolic Logic, doi:https://doi.org/10.1017/jsl.2025. 10(2025), pp. 25

    work page doi:10.1017/jsl.2025 2025

  29. [29]

    ,Second-countable spaces and Reverse Mathematics, Documenta Mathematica, doi: https://doi.org/10.4171/dm/1037(2025), pp. 22

    work page doi:10.4171/dm/1037(2025 2025

  30. [30]

    Simpson,Subsystems of second order arithmetic, 2nd ed., Perspectives in Logic, CUP, 2009

    Stephen G. Simpson,Subsystems of second order arithmetic, 2nd ed., Perspectives in Logic, CUP, 2009

    work page 2009