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. – Simon Henry Jan 4 '18 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. – Mike Shulman Jan 4 '18 at 17:24
• I don't follow your locatedness argument: how do you know when you have a term within $\varepsilon$ of the limit? – François G. Dorais Jan 4 '18 at 17:25
• @FrançoisG.Dorais I don't understand your question. – Mike Shulman Jan 4 '18 at 17:28
• In your argument, you only need the existence of a point that is close enough, but you also need to know it is close enough. I don't see how to know this with out a modulus. – François G. Dorais Jan 4 '18 at 17:35

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? – Mike Shulman Jan 4 '18 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? – Mike Shulman Jan 4 '18 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? – Matt F. Jan 4 '18 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 '18 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. – Mike Shulman Jan 8 '18 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. – Mike Shulman Jan 4 '18 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. – Mike Shulman Jan 4 '18 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. – Carl Mummert Jan 4 '18 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$) – Carl Mummert Jan 4 '18 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. – Carl Mummert Jan 4 '18 at 22:40