The Countable Reals
Andrej Bauer, James E. Hanson
TL;DR
This work constructs a topos in which the Dedekind reals are countable by leveraging parameterized realizability based on a Miller non-diagonalizable sequence, yielding an epimorphism from $N$ onto the real object $R$ in an intuitionistic setting. The core technical tools are parameterized partial combinatory algebras and the associated tripos-to-topos construction, which produce a topos where many analytic results survive while LEM and countable choice fail. The internal analysis shows Brouwer-type fixed-point theorems, the intermediate value theorem, and constraints on real maps (no jumps) within a countable real framework, along with nuanced forms of compactness for $[0,1]$. The results illustrate a striking harmony between constructive logic and classical analysis, revealing which spaces remain countable and how classical-looking theorems manifest without full classical logic.
Abstract
We construct a topos in which the Dedekind reals are countable. The topos arises from a new kind of realizability, which we call parameterized realizability, based on partial combinatory algebras whose application depends on a parameter. Realizers operate uniformly with respect to a given parameter set. Our construction uses a sequence of reals in $[0,1]$, discovered by Joseph Miller, that is non-diagonalizable in the sense that any real which is oracle-computable uniformly from representations of the sequence must already appear in it. When used as the parameter set, this yields a topos in which the non-diagonalizable sequence becomes an epimorphism onto the Dedekind reals, rendering them internally countable. The resulting topos is intuitionistic: it refutes both the law of excluded middle and countable choice. Nevertheless, much of analysis survives internally. The Cauchy reals are uncountable. The Hilbert cube is countable, so Brouwer's fixed-point theorem follows from Lawvere's. The intermediate value theorem and the analytic form of the lesser limited principle of omniscience hold, while the limited principle of omniscience fails. Although no real-valued map has a jump, it remains open whether all such maps are continuous. Finally, the closed interval $[0,1]$, being countable, can be covered by a sequence of open intervals of total length less than any $ε> 0$, with no finite subcover. Yet, we show that any cover using intervals with rational endpoints must admit a finite subcover.