A Model where Dedekind Reals and Cauchy Reals are Different

Question

Is there a model where Dedekind reals and Cauchy reals are different? I'd appreciate if someone can refer me to any related work in case such a model exists.

Answer 1

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.

Answer 2

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}$.

Answer 3

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.

Answer 4

Coincidentally, I am preparing to talk about some of this tomorrow. Here is some of what I will say about this. A good way to think about Dedekind vs Cauchy reals is to think about what kind of information each representation gives.

For Dedekind reals, this is pretty clear: a Dedekind cut for $r$ gives you exactly enough information to determine whether $r \leq q$ or $r \geq q$ for every rational number $q$. Using this information, it is easy to get a Cauchy sequence for $r$. First find an integer $n$ such that $n \leq r \leq n+1$. Then repeatedly bisect the interval $[n,n+1]$, comparing with the midpoint (which is always rational) to determine which half interval to use for the next step. The sequence of midpoints $a_0 = n+1/2, a_1,a_2,\dots$ is a Cauchy sequence for $r$.

For Cauchy reals, we actually get no information at all unless we know something about the rate of convergence of the Cauchy sequence for the real $r$. Since we can easily speed up to a rate of convergence, let's assume that $|a_n - a_{n+1}| \leq 2^{-n}$ for all $n$. What we are given then is a way to get, on input $\varepsilon\gt0$, a (rational) interval of length at most $\varepsilon$ that contains our real number $r$. Can we use this kind of information to get a Dedekind cut for $r$? It's not that easy...

To see that $r \leq q$ we must make sure that $a_n \leq q+2^{1-n}$ for all $n$; similarly, $r \geq q$ happens if and only if $a_n \geq q-2^{1-n}$ for all $n$. To get a Dedekind cut for $r$, we must simultaneously decide which case holds for all rationals $q$. Note that if $r = q$ then both cases hold and we must choose one. Since these decisions could require inspecting the entire Cauchy sequence, we cannot expect to do this in an easy computable manner as we did for the other way around. In fact, there is no computable process which produces a Dedekind cut from such a Cauchy sequence.

In intuitionistic systems, the dichotomy axiom $r \leq 0 \lor r \geq 0$ for Cauchy reals is equivalent to the Lesser Limited Principle of Omniscience (LLPO):

Given $f:\mathbb{N}\to\lbrace0,1\rbrace$ that takes the value $1$ at most once, either $f(2n) = 0$ for all $n$, or $f(2n+1) = 0$ for all $n$.

LLPO is nontrivial and it is not provable in some intuitionistic systems. Even in the presence of LLPO, it is not enough to simply compare $r$ with $0$, we compare the real $r$ with all rationals $q$ and comprehend all these comparisons to form a Dedekind cut for $r$. So a certain nontrivial amount of comprehension is needed on top of LLPO. Since these comparisons are not independent from each other, this is not as hard a requirement as it may seem.

Andrej gave a nice example of a sheaf topos where LLPO fails. In classical systems, LLPO is always true and a very small amount of comprehension is necessary, for example the Spartan subsystem of second-order arithmetic $\mathsf{RCA}_0$ already proves that every Cauchy real (with a known rate of convergence) is equivalent to a Dedekind real. However, the difficulties in converting one representation into another are still visible if the process is repeated infinitely often. See the discussion in Hirst, Representations of reals in reverse mathematics, Bulletin of the Polish Academy of Sciences, Mathematics 55 (2007), 303–316 PDF.

Answer 5

Let me try to fill in some details related to Noah's answer. As Noah mentioned, one can use subsystems of second order arithmetic, such as the theory $\mathsf{RCA}_0$ to talk about reals. The minimal "nice model" of $\mathsf{RCA}_0$ is called $\mathsf{REC}$ and it only includes the (standard) natural numbers and all objects which can be encoded as computable sequences of natural numbers.

Now, to make my answer simpler, rather than using Dedekind cuts, let's consider binary representations of reals. It can be shown in $\mathsf{RCA}_0$ that every Dedekind cut---where the rationals are taken to be above and below---corresponds to a binary real number eg. $10.01110101...$ (It should be noted that this proof is not constructive as it uses the law of excluded middle.)

Since $\mathsf{REC}$ only knows about computable objects, it thinks all binary reals are computable.

Now consider the binary real $h = 0.xxx...$ where $xxx...$ is the Halting problem (i.e. the $e$th bit is $1$ iff the $e$th Turing machine (computer program) halts on input $0$). Note that $h = \sum 2^{-e}$ where the sum is taken over Turning machines $e$ that halt. Let $h_n = \sum 2^{-e}$ where the sum is over Turing machines that halt in $n$ steps. Now $h_n$ is a monotone, bounded, computable sequence of rationals which converges to a noncomputable binary real. (This example is called the Specker sequence.)

However, $\mathsf{RCA}_0$ can show that every monotone bounded sequence of rationals is a Cauchy sequence (that is the usual definition: $\forall \epsilon > 0\ \exists n\ \forall m>n\ |h_m - h_n| \leq \varepsilon$ where $\varepsilon$ is assumed to be rational). The proof is basically an application of pigeonhole principle weak enough to go through in $\mathsf{RCA}_0$.

Hence we have an example of a computable Cauchy sequence (which is provably Cauchy in $\mathsf{RCA}_0$) but for which the model $\mathsf{REC}$ thinks that it has no limit.

(Of course the devil is in the details, and I am sure I am missing a number, but that is the main idea of how you would show it.)

Answer 6

A good reference for this is Fourman and Hyland's 1970 paper on sheaf models for analysis,

Fourman M.P., Hyland J.M.E. (1979) Sheaf models for analysis. In: Fourman M., Mulvey C., Scott D. (eds) Applications of Sheaves. Lecture Notes in Mathematics, vol 753, doi:10.1007/BFb0061823

which I managed to find online here:

https://www.dpmms.cam.ac.uk/~martin/Research/Oldpapers/analysis79.pdf