Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The uncountability of the reals and the Axiom of Choice

Dag Normann, Sam Sanders

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.

The uncountability of the reals and the Axiom of Choice

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: : there is no injection from the unit interval to the natural numbers. We show that relatively strong logical systems cannot prove . 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.
Paper Structure (8 sections, 9 theorems, 10 equations)

This paper contains 8 sections, 9 theorems, 10 equations.

Table of Contents

  1. Introduction
  2. Aim and motivation
  3. Preliminaries
  4. A more negative result
  5. A model of finite type arithmetic
  6. Main result
  7. Some applications
  8. Quantifier-free choice in the base theory

Key Result

Theorem 2.3

Let $A \subseteq {\mathbb N}^{\mathbb N}$ and let $B$ be a set of functionals $F:A \rightarrow {\mathbb N}$. Assume that all $f$ computable in a sequence from $B$ and $A$ are in $A$. Then there is a Kleene closed type structure $\textup{Tp}$ such that $A = \textup{Tp}[1]$ and $B \subseteq \textup

Theorems & Definitions (21)

  • Definition 2.1
  • Definition 2.2: Kleene computability
  • Theorem 2.3
  • Theorem 2.4: Gandy Selection
  • proof
  • Remark 2.5
  • Corollary 2.6
  • proof
  • Lemma 2.7: $\textsf{V = L}$
  • proof
  • ...and 11 more