A Model where Dedekind Reals and Cauchy Reals are Different

With classical logic or countable choice Cauchy and Dedekind reals coincide. Therefore we must look at a model of intuitionistic mathematics without countable choice, such as a topos of sheaves over a space.

For example, let us consider the topos $\mathsf{Sh}(\mathbb{R})$ of sheaves over $\mathbb{R}$ (equipped with the standard topology). The Dedekind reals are the sheaf of continuous real-valued maps, i.e., $$\mathbb{R}_D(U) = \lbrace f : U \to \mathbb{R} \mid f \text{ continuous}\rbrace.$$ The Cauchy reals are the sheaf of locally constant real-valued maps, if I remember correctly.

These two sheaves are not isomorphic. One way to see this: in $\mathbb{R}_C$ the restriction map $\mathbb{R}_C(-1,1) \to \mathbb{R}_C(0,1)$ is a bijection, because every locally constant continuous map $(0,1) \to \mathbb{R}$ is in fact constant, and so is restriction of a constant map $(-1,1) \to \mathbb{R}$. But in $\mathbb{R}_D$ this is not the case, because $x \mapsto 1/x$ is a continuous map $(0,1) \to \mathbb{R}$ which is not the restriction of a continuous map $(-1,1) \to \mathbb{R}$.


In Lubarsky and Rathjen, On the Constructive Dedekind Reals, Proceedings of LFCS '07, Lecture Notes in Computer Science #4514, they construct a model in which the Cauchy reals form a set, but the Dedekind reals are a proper class. Certainly they are different in this case! The model satisfies a modified version of CZF in which the subset collection axiom schema is replaced by the exponentiation axiom.


In Andrej's answer, a "background theory" of something like ZF formulated in intuitionistic logic is assumed. Let me give a slightly different approach.

(EDIT: I did not mean that Andrej's answer used the full power of ZF; I just meant that it seemed to take place in an informal setting with the flavor of ZF. I just wanted to bring up the distinction between the ways in which these separations can happen - for me, the intuitionistic set theory/topos version "feels different" than the reverse math version (I have a very coarse picture of things, here: for me, e.g., ZFC+large cardinals and ETCS give the same, extremely broadly speaking, "picture of the world," which $RCA_0$ does not). I definitely didn't mean to say that Andrej used such-and-such axioms.)

Instead of looking at a set theory, we can approach the question from the perspective of computability theory and reverse mathematics. The theory $RCA_0$ basically consists of "computable" reasoning about natural numbers and sets of natural numbers; for details, see Simpson's book, the first chapter of which is an excellent introduction and motivation for the subject, and is available from his website: http://www.math.psu.edu/simpson/sosoa/chapter1.pdf. $RCA_0$ is the natural base theory to look at if we are interested in the computability side of things, but also want to use classical logic (one might argue that if we care about computability, we shouldn't use classical logic; I don't hold this opinion, but I'm sympathetic to it).

Now, computability theoretically, there are two reasonable notions of "computable Cauchy sequence of rationals": a computable sequence of rational numbers which happens to be a Cauchy sequence classically, or a computable sequence of rational numbers together with a computable function $f$ (a modulus) such that for all rational $\epsilon$, any terms in the sequence after the $f(\epsilon)$th term are $<\epsilon$ apart. These latter sequences can be called "effectively Cauchy," and the statement that every Cauchy sequence has a modulus is equivalent over $RCA_0$ to the much stronger system $ACA_0$.

On the other side of things, there are three reasonable notions of "computable Dedekind cut of rationals": a nonempty computable set of rational numbers which is closed upwards, together with a nonempty computable set of rational numbers which is closed downwards, the two of which are disjoint and omit at most one rational number; a nonempty c.e. set of rational numbers which is closed upwards; or a nonempty c.e. set of rational numbers which is closed downwards. The latter correspond to reals which are "semicomputable from above/below"; see for example http://arxiv.org/pdf/1110.5028.pdf. Again, I believe the equivalence of all these notions is equivalent over $RCA_0$ to $ACA_0$.

Now versions of all of these definitions can be made within $RCA_0$, and appropriate questions about equality can be asked (although one does have to be careful when formalizing these sorts of things). My recollection is that at least one possible version results in $RCA_0$ not proving their equivalence; I'll add the details when I'm more awake.

Tags:

Lo.Logic