Skip to main content
3 of 11
added 1 character in body
Sam Hopkins
  • 24.2k
  • 5
  • 97
  • 171

Please allow me to list some basic observations that might clear up things. I work constructively (without excluded middle) and without the axiom of choice, and assuming powersets are available.

(One can contemplate working in a predicative setting such as CZF, where the Dedekind reals form a class, but I fail to see how it is useful to discuss countability of reals in a setting that does not even allow the formation of reals as a bona fide set.)

Which reals?

There are three standard constructions of reals, which differ constructively:

  • Cauchy reals $\mathbb{R}_c$ are constructed as a quotient of rational Cauchy sequences.

  • Dedekind reals $\mathbb{R}_d$ are constrcuted as (double-sided) Dedekind cuts of rationals.

  • MacNeille reals $\mathbb{R}_m$ are constructed as a certain weaker version of Dedekind cuts of rationals.

We have $\mathbb{R}_c \subseteq \mathbb{R}_d \subseteq \mathbb{R}_m$, where all three inclusions might be proper.

The MacNeille reals fail to satisfy $0 < x \lor x < 1$, which makes them less useful.

Without countable choice, the Cauchy reals are not nice, either. One cannot even show that they are Cauchy-complete.

So the canonical construction for reals is by Dedekind cuts, so most constructive mathematics is done with $\mathbb{R}_d$. (Note also that $\mathbb{R}_c = \mathbb{R}_d$ in the presence of countable choice.)

Countability and subcountability

The definition of countability that works well is: $A$ is countable if there is a surjection $\mathbb{N} \to 1 + A$. When $A$ is inhabited this is equivalent to having a surjection $\mathbb{N} \to A$.

A set $A$ is subcountable if there is $S \subseteq \mathbb{N}$ and a surjection $S \to A$. In particular, every subset of $\mathbb{N}$ is subcountable.

A set $A$ is uncountable if it is not countable. A stronger property is sequence-avoiding: for every sequence $\mathbb{N} \to A$ there is an element of $A$ that is not a term of the sequence.

Theorem: The MacNeille reals are sequence-avoiding, thus uncountable.

Proof. See A constructive Knaster–Tarski proof of the uncountability of the reals by Ingo Blechschmidt and Matthias Hutzler. $\Box$

Theorem: $\lbrace 0, 1\rbrace^\mathbb{N}$ and $\mathcal{P}(\mathbb{N})$ are sequence-avoiding, thus uncountable.

Proof. Cantor's diagonal method is constructive. Given $f : \mathbb{N} \to \lbrace 0, 1\rbrace^\mathbb{N}$, the sequence $n \mapsto 1 - f(n)(n)$ differs from $f(n)$ in the $n$-th place. Similarly, given $g : \mathbb{N} \to \mathcal{P}(\mathbb{N})$, the set $\lbrace n \in \mathbb{N} \mid n \notin f(n) \rbrace$ differs from $f(n)$ at $n$. $\Box$

Caveats:

  1. Constructively the set of binary sequences $\lbrace 0, 1\rbrace^\mathbb{N}$, the powerset $\mathcal{P}(\mathbb{N})$, and the reals (of any kind) cannot be shown to be in bijective correspondence.

  2. It cannot be shown constructively that every real has a digit expansion, so we cannot carry out the diagonal method on $\mathbb{R}$ that way. (This is also a good reason for not teaching uncountability of the reals using decimal expansions. The method of nested intervals is to be preferred, as it works both with excluded middle and countable choice.)

Theorem: If excluded middle holds then $\mathbb{R}_c = \mathbb{R}_d = \mathbb{R}_m$, and they are all sequence-avoiding, thus uncountable.

Proof. See notes from your freshman year in analysis. $\Box$

Theorem: If countable choice holds then $\mathbb{R}_c = \mathbb{R}_d$ and they are both sequence-avoiding, thus uncountable.

Proof. See Bishop's book on constructive analysis, where the method of nested intervals is employed, using countable choice. $\Box$

Contrary to classical mathematics, subcountability has very little to do with countability, apart from the obvious observation that every countable set is subcountable.

Theorem: There is a topos in which there is an injection $\mathbb{R}_d \to \mathbb{N}$ and $\mathbb{R}_d$ is sequence-avoiding, so there is no surjection $\mathbb{R}_d \to \mathbb{N}$.

Proof. This happens in the realizability topos on Joel Hamkins's infinite-time Turing machines. $\Box$

It has also been known since at least the 1980's that in the effective topos $\mathbb{R}_d$ is subcountable and sequence-avoiding.

Further remarks about “sizes” of sets

When you enter the constructive world, you should leave classical ideas about size behind.

Theorem: Suppose the following principle holds: if there are injections $A \to B$ and $B \to A$ then there is a bijection $A \to B$. Then excluded middle holds.

Proof. See Cantor–Bernstein implies Excluded Middle by Chad Brown and Cécilia Pradic. $\Box$

Theorem: Suppose the following principle holds: every subset of a finite set is finite. Then excluded middle holds.

Proof. See the Anger stage of Five stages of accepting constructive mathematics. $\Box$

Theorem: If every subcountable set is countable and Markov principle holds, then excluded middle holds.

Proof. See Proposition 2.6 of Every metric space is separable in function realizability by Andrej Bauer and Andrew Swan. $\Box$

Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 240