The Countable Reals

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 $\epsilon > 0$, with no finite subcover. Yet, we show that any cover using intervals with rational endpoints must admit a finite subcover.