Cauchy real numbers with and without modulus

Question

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?

Answer 1

I don't see an algebraic difference. Even in constructive math without countable choice, we can define the total functions $+, -, \times, \min, \max, \sqrt[3]{}$ 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.

Answer 2

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.