Cantor's theorem about uncountability of the reals can be proved using excluded middle or countable choice. But can it be proved without either of them? I will present joint work with James E. Hanson in which we give the answer by constructing a topos, i.e., a model of intuotionistic higher-order logic, in which the Dedekind reals are countable. There are two main ingredients:
• A result in computability theory, established by Joseph S. Miller, that there exists a sequence of reals against which oracle Turing machines cannot diagonalize uniformly in the oracle representing the sequence. The theorem relies on a generalization of Brouwer's fixed point theorem to the Hilbert cube and multi-valued continuous maps whose images are closed convex sets.
• A new variant of realizability, which we call uniform realizability that embodies the uniform oracle computations used in Miller's sequences.
In this talk I will present the general ideas, the construction of Miller's sequences, and outline uniform realizability.