Last year, Andrej Bauer [gave a talk](https://www.youtube.com/watch?v=4CBFUojXoq4&list=FLuLR2oAJOXHh0nBVDDuj3Lg&index=24&t=71s) showing that there is a topos in which the set of Dedekind reals is (sub)countable, and thus, you cannot prove that $\mathbb{R}$ is uncountable without LEM. He claims in [this abstract](https://researchseminars.org/talk/ToposInstituteColloquium/57/) that this was an open problem. However, [it was already known](https://mathoverflow.net/questions/410703/subcountability/410755?_gl=1*8q3akn*_ga*NDIwNzk0NDg2LjE2NDA5NzU5Njg.*_ga_S812YQPLT2*MTY5MjgwMzczMC4yOTguMS4xNjkyODA0MzQzLjAuMC4w#410755) that it is consistent with CZF that every set (and in particular, the Dedekind reals) is subcountable. So is Bauer's and Hanson's result actually new?


Also note that Bauer's and Hanson's result is not yet published, but it should supposedly be published soon according to [Bauer's blog](https://math.andrej.com/).


Edit: Thanks to the answers by Andrej Bauer and James Hanson, I have realized my biggest misunderstanding. I for some reason implicitly thought subcountability and countability are equivalent, but this is not the case in the intuitionist setting. Thus, the consistency of the Dedekind reals being subcountable does not yield that it is consistent that the Dedekind reals are countable.


Something else several others pointed out is that CZF is a generally weaker system than "ZFC without choice or LEM". So, even if the question were to be solved in CZF, this wouldn't mean the question "Can the real numbers be shown uncountable without excluded middle and without the axiom of choice?" was really settled. Bauer's and Hanson's topos construction gives a negative answer in the setting of higher-order intuitionist logic (and in IZF as per Hanson's comment).


Thanks again to everyone for sharing your input!



Is Bauer–Hanson’s result “there is a topos where the Dedekind reals are countable” novel?
Please allow me to list some basic observations that might clear up things. I work constructively (without excluded middle) and without the axiom of choice, and assuming powersets are available.


(One can contemplate working in a predicative setting such as CZF, where the Dedekind reals form a class, but I fail to see how it is useful to discuss countability of reals in a setting that does not even allow the formation of reals as a bona fide set.)


#### Which reals?


There are three standard constructions of reals, which differ constructively:


* **Cauchy reals** $\mathbb{R}\_c$ are constructed as a quotient of rational Cauchy sequences.
* **Dedekind reals** $\mathbb{R}\_d$ are constrcuted as (double-sided) Dedekind cuts of rationals.
* **MacNeille reals** $\mathbb{R}\_m$ are constructed as a certain weaker version of Dedekind cuts of rationals.


We have $\mathbb{R}\_c \subseteq \mathbb{R}\_d \subseteq \mathbb{R}\_m$, where all three inclusions might be proper.


The MacNeille reals fail to satisfy $0 < x \lor x < 1$, which makes them less useful.


Without countable choice, the Cauchy reals are not nice, either. One cannot even show that they are Cauchy-complete.


So the canonical construction for reals is by Dedekind cuts, so most constructive mathematics is done with $\mathbb{R}\_d$. (Note also that $\mathbb{R}\_c = \mathbb{R}\_d$ in the presence of countable choice.)


### Countability and subcountability


The definition of countability that works well is: $A$ is **countable** if there is a surjection $\mathbb{N} \to 1 + A$. When $A$ is inhabited this is equivalent to having a surjection $\mathbb{N} \to A$.


A set $A$ is **subcountable** if there is $S \subseteq \mathbb{N}$ and a surjection $S \to A$. In particular, every subset of $\mathbb{N}$ is subcountable.


A set $A$ is **uncountable** if it is not countable. A stronger property is **sequence-avoiding**: for every sequence $\mathbb{N} \to A$ there is an element of $A$ that is not a term of the sequence.


**Theorem:** *The MacNeille reals are sequence-avoiding, thus uncountable.*


*Proof.* See [A constructive Knaster–Tarski proof of the uncountability of the reals](https://arxiv.org/abs/1902.07366) by Ingo Blechschmidt and Matthias Hutzler. $\Box$


**Theorem:** *$\lbrace 0, 1\rbrace^\mathbb{N}$ and $\mathcal{P}(\mathbb{N})$ are sequence-avoiding, thus uncountable.*


*Proof.* Cantor's diagonal method is constructive. Given $f : \mathbb{N} \to \lbrace 0, 1\rbrace^\mathbb{N}$, the sequence $n \mapsto 1 - f(n)(n)$ differs from $f(n)$ in the $n$-th place. Similarly, given $g : \mathbb{N} \to \mathcal{P}(\mathbb{N})$, the set $\lbrace n \in \mathbb{N} \mid n \notin f(n) \rbrace$ differs from $f(n)$ at $n$.
$\Box$


Caveats:


1. Constructively the set of binary sequences $\lbrace 0, 1\rbrace^\mathbb{N}$, the powerset $\mathcal{P}(\mathbb{N})$, and the reals (of any kind) *cannot* be shown to be in bijective correspondence.
2. It cannot be shown constructively that every real has a digit expansion, so we cannot carry out the diagonal method on $\mathbb{R}$ that way. (This is also a good reason for *not* teaching uncountability of the reals using decimal expansions. The method of nested intervals is to be preferred, as it works with either excluded middle or countable choice.)


**Theorem:** *If excluded middle holds then $\mathbb{R}\_c = \mathbb{R}\_d = \mathbb{R}\_m$, and they are all sequence-avoiding, thus uncountable.*


*Proof.* See notes from your freshman year in analysis. $\Box$


**Theorem:** *If countable choice holds then $\mathbb{R}\_c = \mathbb{R}\_d$ and they are both sequence-avoiding, thus uncountable.*


*Proof.* See for example Bishop's book “Foundations of constructive analysis" (1967, Section 2.2), where the method of nested intervals is employed, using countable choice. $\Box$


Contrary to classical mathematics, subcountability has very little to do with countability, apart from the obvious observation that every countable set is subcountable.


**Theorem:** *There is a topos in which there is an injection $\mathbb{R}\_d \to \mathbb{N}$ and $\mathbb{R}\_d$ is sequence-avoiding, so there is no surjection $\mathbb{N} \to \mathbb{R}\_d$.*


*Proof.* This happens in the realizability topos on Joel Hamkins's infinite-time Turing machines. I have not actually written this down, but the embedding is done much the same way as the embedding $\mathbb{N}^\mathbb{N} \to \mathbb{N}$ in [An injection from the Baire space to natural numbers](https://doi.org/10.1017/S0960129513000406). The idea is that infinite-time Turing machines can compute from any code of a rational Cauchy sequence converging to $x$ a canonical such code. $\Box$


It has also been known since at least the 1980's that in the effective topos $\mathbb{R}\_d$ is subcountable and sequence-avoiding.


### Further remarks about “sizes” of sets


When you enter the constructive world, you should leave classical ideas about size behind.


**Theorem:** *Suppose the following principle holds: if there are injections $A \to B$ and $B \to A$ then there is a bijection $A \to B$. Then excluded middle holds.*


*Proof.* See [Cantor–Bernstein implies Excluded Middle](https://arxiv.org/abs/1904.09193) by Chad Brown and Cécilia Pradic. $\Box$


**Theorem:** *Suppose the following principle holds: every subset of a finite set is finite. Then excluded middle holds.*


*Proof.* See the Anger stage of [Five stages of accepting constructive mathematics](http://dx.doi.org/10.1090/bull/1556). $\Box$


**Theorem:** *If every subcountable set is countable and Markov principle holds, then excluded middle holds.*


*Proof.* See Proposition 2.6 of [Every metric space is separable in function realizability](https://doi.org/10.23638/LMCS-15%282%3A14%292019) by Andrej Bauer and Andrew Swan. $\Box$


