Is Bauer–Hanson’s result “there is a topos where the Dedekind reals are countable” novel?

Question

Last year, Andrej Bauer gave a talk 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 that this was an open problem. However, it was already known 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.

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!

Answer 1

[Update 2024-04-15: The preprint The countable reals is now available.]

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.

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 constructed 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. For an inhabited set, 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 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 $g(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. 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 1980s 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 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. $\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 by Andrej Bauer and Andrew Swan. $\Box$

Answer 2

In the topos we construct in our paper there is a surjection/epimorphism from the natural numbers to the Dedekind reals. In the model of CZF you mention (and in the effective topos) the Dedekind reals are subcountable, meaning that there is a surjection from a subset of the natural numbers to the Dedekind reals. Externally this subset has non-trivial computational complexity (corresponding roughly to the set of Turing indices of total computable functions), so the situation in the new topos is more special.

One way to see how this is subtle is that it is known by a result of Blechschmidt and Hutzler, in A constructive Knaster–Tarski proof of the uncountability of the reals, that the MacNeille reals are uncountable in any topos. Also Cantor's diagonal argument and similar give that Cantor space and Baire space (and therefore the set of irrational Dedekind reals) are always uncountable, even when they are also subcountable. (And to clarify, I mean uncountable in the positive, constructive sense that given any sequence of elements one can construct an element not on the list.)

There's also some really bizarre specific cases in our topos: The (Dedekind) interval $[0,1]$ is countable, the Hilbert cube $[0,1]^\omega$ is countable, the circle $S^1$ is countable, but $(S^1)^\omega$ is uncountable (by Lawvere's fixed-point theorem). Also the Cauchy reals are uncountable despite the fact that the Cauchy reals in this topos are externally isomorphic to the Dedekind reals. And indeed there is internally a 'sub-two-to-one' map from the Cauchy reals to the Dedekind reals, so the Dedekind reals are one application of 'countable choice for sub-pairs' from being uncountable.

Incidentally given that the construction is a modification of the standard construction of the effective topos, it should be a fairly trivial matter to modify it to give a construction of a model of IZF (and therefore also of CZF) in which the Dedekind reals are countable.

Answer 3

A first big difference between Brauer & Hansen's result and the one you are talking about is that CZF is a predicative theory (it doesn't have power set/power object) so consistency with CZF doesn't say anything about what is possible in a topos. The internal logic of toposes has more to do with IZF, or rather something like IZF with bounded replacement. For example:

• It's not clear that the Dedekind reals are even definable in CZF. (though it seems it is possible - see the comment by David Roberts below).

• The usual Cantor diagonal argument shows that it is not consistent (say in IZF or in a topos) that $\mathcal{P}(\mathbb{N})$ is subcountable (as in "is a subquotient of $\mathbb{N}$"). But $\mathcal{P}(\mathbb{N})$ doesn't exist in CZF so it's fine, but it shows that it is inconsistent with IZF that every object is subcountable.

Edit: However, as pointed out by Andrej in the comments 1 2 — that's not where the new contribution of their result lies: Independently of the result cited in the OP. It was already known that the Dedekind reals can be sub-countable in a topos (and that it is consistent with IZF) — this holds in the effective topos. So depending on which classically equivalent definition of "countable" and of "the reals" you are using, it was already known that "You cannot prove he reals are uncountable in IZF(that is ZFC without AC and LEM)". The new contribution lies in the difference between "countable" which means being a quotient of the natural numbers and "subcountable" which means "being a quotient of a subobjects of the natural numbers" or equivalently, "being a subset of a countable set". Without LEM there is a big difference between these two notions! In intuitionistic mathematics, a subset can be much more complicated that the set itself. For example, a subset of a finite set doesn't have to be finite.

Answer 4

Against my better judgement, I would answer your question in the negative.

My motivation is that even rather strong classical theories cannot prove that

"there is no injection from Cantor space (or: the real numbers using your favourite representation, or: Baire space) to the natural numbers" (NIN)

The relevant results due to Dag Normann and myself may be found here:

https://arxiv.org/abs/2007.07560

In particular, the above NIN is not provable in Z$_2^\omega$+QF-AC$^{0,1}$, which consists of

1. Kohlenbach's base theory of higher-order RM (RCA$_0^\omega$, which is classical).

2. Functionals S$_k^2$ that decide all $\Pi_k^1$-formulas (for any $k$)

3. countable choice for quantifier-free formulas (QF-AC$^{0,1}$)

As suggested by its notation, the system Z$_2^\omega$ proves the same second-order sentences as Z$_2$, i.e. second-order arithmetic.