It opens:
> 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.