Is any Cauchy sequence for completion of rational semicomputable?

Question

For the definition of a semicomputable real, see An Introduction to Kolmogorov Complexity and its Applications by Li and Vitanyi (1997). In fact, it is not true that every Cauchy sequence for completion of rationals is semicomputable, we can not complete rationals by semicomputable Cauchy sequences.

My question:

1. how could we, in a Constructivist way based on Cauchy sequences, complete the rational number system? Specifically, how to overcome the non-computable problem of some (in fact, uncountably many) Cauchy sequences by which to complete the rational system?

2. Since we complete the rational number system in several ways like Cauchy seqences, Dedekind cuts or even by continued fractions, what is the common ideas (of approach, etc) among them?

Answer 1

Constructions of real numbers broadly fall into two classes: Dedekind-style completions by cuts ("Dedekind reals"), and Cauchy-style completions by Cauchy sequences ("Cauchy reals"). There is a well understood theory of these in constructive mathematics, and the connections between the different constructions are well known.

In general, the Cauchy reals form a subfield of the Dedekind reals. The Dedekind and Cauchy reals coincide if countable choice or excluded middle holds, but may otherwise be different. You can read about these things in Troelstra and van Dalen's Constructivism in mathematics, Vol. 1.

You ask specifically about the Cauchy completion of rationals and the "non-computable problem". There is no such problem. When we work in intuitionistic logic, we simply construct the Cauchy reals like we always do:

1. Start with rational numbers $\mathbb{Q}$.
2. Use the usual definition of Cauchy sequence.
3. Let $\mathcal{C}$ be the set of all rational Cauchy sequences.
4. Define two Cauchy sequences $(q_n)_n$ and $(r_n)_n$ to be equivalent, written $(q_n)_n \approx (r_n)_n$ when for every $\epsilon > 0$ there is $n \in \mathbb{N}$ such that for all $m, k \geq n$ we have $|q_m - r_k| < \epsilon$.
5. Let $\mathbb{R}$ be the quotient $\mathcal{C}/{\approx}$.

We can prove, still working in intuitionistic logic, that $\mathbb{R}$ forms an archimedean ordered field (although the axioms of order need to be phrased carefully). If we have countable choice (which we usually do in constructive mathematics) then we can also show that $\mathbb{R}$ is Cauchy complete. We get all the usual structure.

The important thing to understand here is that when we work constructively we do not speak about computable or non-computable objects. We just do math as usual, except we do not assume the law of excluded middle.

Questions about computability and non-computability become possible when we consider models of constructive mathematics. Let us look at several models and see how the Cauchy reals work in them:

1. Classical set theory: classical mathematics is a special case of constructive mathematics, and so everything is as usual. There are non-computable reals and non-computable Cauchy sequences.

2. The effective topos: in this model everything is computable. The object $\mathbb{R}$ consists of computable reals, and only computable Cauchy sequences exist. Note that "computable Cauchy sequence" means two things: that the sequence is computable and that "is Cauchy" is computable as well.

3. The relative realizability topos $\mathrm{RT}(K_2, K_2^{\mathrm{eff}})$ over Kleene's second algebra and its computable subalgebra. It is not important what the details of this topos are but what we get is: the object $\mathbb{R}$ consists of all reals, the object $\mathcal{C}$ of Cauchy sequences consists of all Cauchy sequences, but all operations in the topos are computable. (Yes, it is possible to compute with non-computable reals!)

There are many other models, but always the same thing happens: what real numbers are depends on what Cauchy sequences are, and that depends on the details of the model. In all cases, things fit together: you cannot have a model with non-computable Cauchy sequences and only computable real numbers.

Answer 2

I wonder if there is constructive theories of the real which is based on Cauchy sequence, specifically, how to overcom the non-computable problem of some (in fact,uncountably many) Cauchy sequence by which to complete rationals system.

Yes, there are constructive theories of the real line which use a form of Cauchy sequences. In general, these theories will not prove that every real number is computable. The assumption that every real number is computable is a form of what is called Church's thesis in that context (this is not quite the same as the usual Church-Turing thesis).

One example is the constructive system used by Bishop, named BISH in Varieties of Constructive Mathematics by Bridges and Richman (1987). In BISH, a real number is taken to be a Cauchy sequence of rationals with a fixed modulus of convergence. These are called "quickly converging Cauchy sequences" in some contexts such as Simpson's book on reverse mathematics. So we might assume, for example, that if we take $\epsilon = 1/m$ in the definition of a Cauchy sequence then we can take $N$ to be simply $m+1$.

BISH is compatible with the assumption that every real number is computable, but at the same time his system cannot prove that every real number is computable. BISH can prove that there is no single sequence $(x_1, x_2, \ldots)$ that contains every real number, and so it proves the reals are uncountable in that sense.

Perhaps part of the intuition is that, even if a constructive system cannot prove that "every real number is computable", it is still probably the case that if a specific real number is constructed without any assumptions, that real number will be computable (this kind of metatheorem can often be proved about a formal constructive system using the "realizability" method).

Furthermore, if a real number is generated in a constructive system using some extra assumptions, it will often be the case that if the objects in the assumption are all computable then the real number being generated will also be computable. So all the specific real numbers encountered in practice in these theories will be computable, even if the theory cannot prove that every real number is computable.

One strength of not proving that every real number is computable is that constructive systems such as Bishop's are compatible with classical mathematics: any proof in Bishop's system is also a classically correct proof. Of course there is no classically correct proof that all real numbers are computable, so any constructive system that can prove that will be incompatible in some cases with classical reasoning.