The countable reals

Abstract: Joint work with James E. Hanson from the University of Maryland, james-hanson.github.io.

In 1874 Georg Cantor published a theorem stating that every sequence of reals is avoided by some real, thereby showing that the reals are not countable. Cantor's proof uses classical logic. There are constructive proofs, although they all rely on the axiom of countable choice. Can the real numbers be shown uncountable without excluded middle and without the axiom of choice? An answer has not been found so far, although not for lack of trying.

We show that there is a topos in which the real numbers are countable, i.e., there is an epimorphism from the object of natural numbers to the object of Dedekind reals. Therefore, higher-order intuitionistic logic cannot show the reals to be uncountable.

The starting point of our construction is a sequence of reals, shown to exist by Joseph S. Miller from University of Wisconsin–Madison, with a strong counter-diagonalization property: if an oracle Turing machine computes a specific real number, when given any oracle representing Miller's sequence, then the number appears in the sequence. One gets the idea that the reals ought to be countable in a realizability topos built from Turing machines with oracles for Miller's sequence. However, we cannot just use ordinary realizability, because all realizability toposes validate countable choice and consequently the uncountability of the reals.

To obtain a topos with countable reals, we define a variant of realizability which we call parameterized realizability. First we define parameterized partial combinatory algebras (ppca), which are partial combinatory algebras whose evaluation depends on a parameter. We then define parameterized realizability toposes. In these realizers witness logical statements uniformly in the parameters. The motivating example is the parameterized realizability topos built from the ppca of oracle Turing machines parameterized by oracles for Miller's sequence. In this topos, Miller's sequence is the desired epimorphism from natural numbers to Dedekind reals.

Computer sciencealgebraic topologycategory theorylogic

Audience: learners

( chat )

Topos Institute Colloquium