# Cauchy real numbers with and without modulus

In constructive mathematics there are many possible inequivalent definitions of real numbers. The greatest variety seems to be in Dedekind-style approaches: in addition to "the" Dedekind real numbers which satisfy locatedness (for all $q<r$ in $\mathbb{Q}$, either $x<r$ or $q<x$), there are the MacNeille, upper, and lower reals, and perhaps others. It is easy to construct models distinguishing between all these: for instance, in a topos of sheaves on a space $X$, the Dedekind reals are the sheaf of continuous $\mathbb{R}$-valued functions on $X$, the upper and lower reals are respectively the sheaves of upper and lower semicontinuous $\mathbb{R}$-valued functions on $X$, and the MacNeille reals are the sheaf of pairs of upper and lower semicontinuous functions satisfying a closeness condition. This gives me a good topological intuition for the difference between these definitions.

This question is about an analogous possible variation in Cauchy-like real numbers. Classically, a sequence $(x_n)$ of rational numbers is Cauchy if $\forall k \exists n \forall p,q>n. |x_p-x_q|<2^{-k}$. But almost without exception, constructive mathematicians define Cauchy sequences by "building a Skolem function" into the definition, assuming that there is a "modulus of Cauchy-ness" $N:\mathbb{N}^{\mathbb{N}}$ such that $\forall k \forall p,q > N_k. |x_p-x_q|<2^{-k}$. And once one has such a modulus, one can massage the sequence $(x_n)$ to make the modulus coincide with a standard one such as $N_k = k$.

My question is: what is the difference in constructive mathematics between Cauchy real numbers having a modulus of Cauchy-ness and without it? It seems to me that the no-modulus Cauchy reals sit in between the with-modulus Cauchy reals and the Dedekind reals; we shoudn't need a modulus to get locatedness, all we need is the existence of some point of the sequence that's closer than $\frac{|q-r|}{2}$ to the limit so we can compare it to $q$ and $r$.

I understand that someone who cares about algorithms and computation will want a modulus to compute with, but if I am a topologist and am happy with Dedekind reals, leaving out a modulus in the Cauchy reals is not a priori a bad thing to do. Are the no-modulus Cauchy reals any less well-behaved intrinsically than the with-modulus ones? Is their algebraic and order structure any different? And are there (hopefully topological) models (necessarily failing countable choice) that distinguish the no-modulus Cauchy reals from both the with-modulus ones and from the Dedekind reals?

• If I remember correctly, the problem with Cauchy real without modulus is that in general you can't apply the usual diagonal process showing that a Cauchy sequence of Cauchy real converge to a Cauchy real... This makes their study quite limited. Also it is indeed true that any Cauchy real (with or without modulus) is a Dedeking real. Jan 4, 2018 at 16:53
• @SimonHenry You can't do that for Cauchy reals with modulus either unless you assume countable choice (thereby collapsing the Dedekind reals to the Cauchy reals as well), since a Cauchy sequence of Cauchy reals is a sequence of equivalence classes of Cauchy sequences. Jan 4, 2018 at 17:24
• I don't follow your locatedness argument: how do you know when you have a term within $\varepsilon$ of the limit? Jan 4, 2018 at 17:25
• Just to clarify the terminology: am I understanding right that by “with-modulus”, you don’t mean “equipped with a modulus”, but rather “such that a modulus exists”? Jan 4, 2018 at 17:43
• @PeterLeFanuLumsdaine Haha, good question! Certainly a given Cauchy sequence should represent the same real number no matter which modulus you give it. We're already passing to equivalence classes of Cauchy sequences in defining the Cauchy reals, so the question is about comparing equivalence classes of Cauchy sequences for which there exists a modulus to equivalence classes of Cauchy sequences equipped with a modulus. But I think these are isomorphic, as long as we have the function comprehension (unique choice) principle. Jan 4, 2018 at 17:49

I don't see an algebraic difference. Even in constructive math without countable choice, we can define the total functions $+, -, \times, \min, \max, \sqrt{}$ and the partial functions $1/x, \sqrt{x}$ on the no-modulus Cauchy reals.

However, there is a difference in that Cauchy completeness does not hold for the no-modulus reals. Consider the situation in the recursive topos or in recursive mathematics:

• Let $R$ be the no-modulus Cauchy reals, considered as functions $r : N \rightarrow Q$.
• Let $S$ be the set of with-modulus Cauchy sequences of no-modulus reals, considered as functions $s : N \rightarrow R$, such that $\forall m, m', |s(m)-s(m')| < 1/m + 1/m'.$
• Suppose (for contradiction) that $\forall s \in S\ \exists r \in R\ \lim s=r$.
• Then there would be a recursive function $f:S\rightarrow R \ \lim s=f(s)$.
• Now consider $s=0^S$, i.e. the sequence such that $\forall n\ s(n)=0^R$, i.e. the sequence such that $\forall n\forall m\ s(n)(m)=0^Q$. The calculation of $(f(s))(1)$ uses at most $k_1$ terms of $s$, the calculation of $(f(s))(2)$ uses at most $k_2$ terms of $s$, etc.
• Let $t(n)(m)=0$ if $n+m < k_{n+m}$, and 1 otherwise. Then $t$ is in $S$.
• Then $f(s)=f(t)$, but $\lim s = 0$ and $\lim t=1$, which is a contradiction.

If we tried to replace $R$ and $S$ by the with-modulus Cauchy reals and sequences thereof, we would find that $t(1)$ might not be a with-modulus real, $t$ might not be in the new $S$, and the argument would not go through.

So in the recursive world: the with-modulus reals lead to all Cauchy sequences converging; the no-modulus reals lead to Cauchy sequences that may not converge.

• This is an interesting argument. In general I don't know of any way to prove that the with-modulus Cauchy reals are Cauchy complete without using countable choice, which already collapses the Dedekind reals to the with-modulus Cauchy reals. You seem to be saying there is a particular model in which the with-modulus Cauchy reals don't coincide with the Dedekind reals, but happen to nevertheless be Cauchy complete, while the no-modulus ones aren't; is that right? Jan 4, 2018 at 17:26
• Is there a logical principle that implies Cauchy completeness of the with-modulus Cauchy reals but is weak enough to keep them distinct from the no-modulus ones? Jan 4, 2018 at 17:27
• @MikeShulman, when you said "almost without exception, constructive mathematicians...", I think it was fair to assume no equivalence classes. So perhaps you might post a separate question, like this: Let's work in the context of constructive mathematics without countable choice. Consider E = Cauchy sequences of rationals with explicit modulus and F = Cauchy sequences of rationals with free modulus. Consider the corresponding sets of equivalence classes E* and F*. Obviously there is no canonical isomorphism between $(E^*,+,*,<)$ and $(F^*,+,*,<)$. But what properties distinguish the two? Jan 4, 2018 at 20:55
• For more on the subject of properties of Cauchy sequences (as opposed to reals), see doi.org/10.1016/j.entcs.2006.09.012
– Dap
Jan 5, 2018 at 6:37
• @Dap Thank you!! Could you please post that paper in an answer to the question, not just in a comment? It doesn't exactly address the question I asked, but it's highly relevant and very comprehensive in what it does address. Jan 8, 2018 at 19:12

Let $(a_n)$ be a Specker sequence - a computable, bounded, increasing sequence of rationals so that the limit is not a computable real.

First, assume for simplicity that we work in any system of second-order arithmetic (classical or not) that has REC as a model. This is the model with the standard natural numbers and the computable sets of natural numbers. In this model, the Specker sequence is a non-modulus Cauchy sequence (because it is a Cauchy sequence in the standard model, and being Cauchy is defined arithmetically). But there is no computable modulus of convergence for a Specker sequence, so the model does not believe that the sequence is a modulus Cauchy sequence.

Thus our system cannot prove that "every non-modulus Cauchy sequence has a modulus". Systems affected by this include many systems of constructive second-order arithmetic as well as the classical system $\mathsf{RCA}_0$.

In fact, every modulus of a Specker sequence computes $\emptyset'$. So the previous argument also goes through for any system of second-order arithmetic (classical or not) that has a $\omega$-model without any Turing complete reals. This applies to $\mathsf{WKL}_0$ and to constructive systems with various forms of compactness.

Similar arguments will work for systems that are not fragments of second-order arithmetic, as long as they have $\omega$-models that do not contain any Turing complete reals.

• Thanks! I find it easier to think about toposes, but presumably there is a realizability topos containing a Specker sequence in which the same argument works. But what I would really understand much better is a topological model. Jan 4, 2018 at 17:39
• Hmm... I don't know much about recursive models, but I'm looking at the construction of a Specker sequence in Troelstra and van Dalen, and it looks to me as though it proves that if $f:\mathbb{N}\to\mathbb{N}$ is injective and $r_k = \sum_{i=0}^k 2^{-f(i)}$, and if $(r_k)$ is no-modulus Cauchy, then the image of $f$ is decidable -- from which I think one can deduce that $(r_k)$ in fact converges and is with-modulus Cauchy. So I don't understand how a Specker sequence can be no-modulus Cauchy. Jan 4, 2018 at 19:53
• @Mike Shulman: it's a bounded increasing sequence of rationals, so classically it is a Cauchy sequence (ignoring the issue of a modulus). Because the sentence expressing that this Specker sequence is (no-modulus) Cauchy is arithmetical, and because the definition of the sequence itself is arithmetical, this means that every $\omega$-model will believe that the sequence is no-modulus Cauchy. Jan 4, 2018 at 21:53
• Looking at Troelstra and van Dalen p. 268, to show that the image of $f$ is computable using their construction requires a modulus. They say "then for any $m$ we can find a $k$ with ..." - but in order to compute the range of $f$ we would need to compute $k$ from $m$, which is to say we need a computable modulus. (They are also working in the context of $\text{CT}_0$ there, but this is primarily to bridge the gap between the constructive meaning of "decidable" and the computable meaning. The range of $f$ does not exist in REC, which does not satisfy $\text{CT}_0$) Jan 4, 2018 at 22:14
• Indeed, they comment on p. 193 that $\text{CT}_0$ is equivalent to saying that the function implicitly defined by an arithmetical $(\forall n)(\exists m)$ statement is always computable; finding the modulus of a Specker sequence is just a special case of this. Jan 4, 2018 at 22:40