A Model where Dedekind Reals and Cauchy Reals are Different

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.

-
I think an important point which you need to clarify is what you mean by "model" - in particular, "model of what" and "model in what sense" For instance, I believe there are toposes in which the two notions differ; would you count those as "models"? – Noah Schweber Apr 24 '13 at 5:01
It's also necessary to be very specific about what you mean by a Dedekind real. The original definition, due to Dedekind, is that a Dedekind real is a certain kind of partition of $\mathbb{Q}$, but that is not the definition typically used in constructive mathematics. This difference in terminology can cause significant confusion when trying to compare different results about "Dedekind reals". – Carl Mummert Apr 24 '13 at 17:32
As you can see in the answers, the same confusion that Carl mentioned about "Dedekind" also arises with "Cauchy". Is a rate of convergence (modulus) included in the definition? This can lead to very different results when working with weak theories like constructive math and subsystems of second order arithmetic. Takeaway: definitions which are equivalent in stronger theories can be separated in weaker theories. – Jason Rute Apr 24 '13 at 18:54
Gerald, that doesn't make sense at this point. The outcome would be to invalidate all but at most one of the excellent answers below. – François G. Dorais Apr 24 '13 at 19:52
You won't find a model of ZF where they are different but there are models of IZF where they are different. There are several types of Dedekind cuts: left/right open or ambivalent? Decidable, located or arbitrary? Same for Cauchy sequences: fixed or arbitrary convergence rate? Different combinations give radically different answers. – François G. Dorais Apr 25 '13 at 4:18

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.

-
This is strange. It seems they are including the modulus in the definition of Cauchy sequence, which is why the Cauchy definition is so strong. However, what makes the Dedekind definition so weak? I'm missing something here. – Jason Rute Apr 24 '13 at 18:50
@Jason I think the main issue is that Cauchy sequences are functions, whereas Dedekind cuts are subsets. In this model the power "set" of the naturals is also a proper class. – aws Apr 24 '13 at 19:29
Indeed, in constructive settings there is a whole lot of difference between $2^\omega$ and $\mathcal{P}(\omega)$. Note that the Dedekind cuts in Lubasrsky & Rathjen are located but not necessarily decidable. – François G. Dorais Apr 24 '13 at 22:45

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

-
Andrej's answer only needs a category of sets, not IZF. ETCS is more than sufficient. – David Roberts Apr 24 '13 at 7:45
I am not particularly amused when a "background theory" is imposed on an informal argument which I make. It is the logicians' wishful thinking that informal mathematics stands on formal mathematics. But since you raised the issue, possible backgrounds for my answer could be ZFC, IZF, ETCS, IHOL, BZ, or HOTT. Take your pick. – Andrej Bauer Apr 24 '13 at 9:05
I think Noah's point is that you don't even need that much background. Some flavor of second-order arithmetic is enough. – François G. Dorais Apr 24 '13 at 10:24
The models are models of different things. Noah says the Dedekind and Cauchy reals can differ in a model of $RCA_0$, while Andrej shows they can differ in models of any of the far stronger background theories he lists. Noah says computability considers can block the proof of equivalance while Andrej notes continuity conditions can. As far as the meta-theoretic assumptions of the two proofs, those are probably identical. – Colin McLarty Apr 24 '13 at 14:00
@Andrej, Yes, you see yourself as building categories of sheaves at a level like ZFC or HOTT but not using any specific metatheory. This makes it transparent that the two kinds of reals can differ in models of relatively strong (but 'intuitionistic') formal theories like IZF. This is like Cohen presenting forcing as building forcing conditions in ZFC. But Cohen also notes a fragment of arithmetic suffices as metatheory to formalize the reasoning and verify the (non-)deducibility of AC or CH from ZF axioms. I think there is room to talk about both formal systems and ideas. – Colin McLarty Apr 24 '13 at 15:54

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.

-
François, you say $\mathsf{𝖱𝖢𝖠}_0$ already proves that every Cauchy real is equivalent to a Dedekind real. But this is only true if you take the fast Cauchy sequence definition (where the rate of convergence is given). If one uses the usual definition, then they can not be proved equivalent over $\mathsf{𝖱𝖢𝖠}_0$. – Jason Rute Apr 24 '13 at 18:13
Thanks Jason, I thought that was implied from the third paragraph but I will edit for clarity. – François G. Dorais Apr 24 '13 at 18:25
It's a pity that you write $\leq$, where $\lt$ would be better since it is an observable property. – Paul Taylor Apr 18 at 19:05
@PaulTaylor: I'm not sure I understand. $\mathsf{LLPO}$ is definitely about non-observable properties. In other words, it says either you can't observe one or you can't observe the other. If it were about observable properties, it would be constructively true! – François G. Dorais Apr 18 at 20:46
Using $\lt$ makes your first four paragraphs constructive, apart from the word "determines", but you can fix that by using overlapping intervals (such as signed binary) and being non-deterministic about the Cauchy sequence, with Dependent Choice. I think this deals with the problems in the second half of your post, although I don't really understand it since I wouldn't do it that way. See The Dedekind Reals in ASD by Andrej and me. – Paul Taylor Apr 18 at 21:18

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.)

-

A good reference for this is Fourman's 1970 paper on sheaf models for analysis, which I managed to find online here,

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

-