Skip to main content
2 of 4
added 599 characters in body
James E Hanson
  • 13.2k
  • 3
  • 38
  • 72

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 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 uncoutnable, 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's 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.

James E Hanson
  • 13.2k
  • 3
  • 38
  • 72