# Is there a “nice” “constructive” field of numbers?

I am wondering about this. I've had some interest in “constructive” mathematics, although also some rather strong opinions against those who want to insist that everything else is “wrong” in favor of it.

One constructive object is the “computable real number line” as an alternative to the usual Cantor-Dedekind real number line. The computable real number line is such that the numbers on it are all “computable”, meaning you can give an algorithm (perhaps extremely long and inefficient) which will compute the number and which can be run by a Turing computer. In particular, noncomputable constants, like Chaitin's Omega, simply don't exist.

The approach is appealing, since it means you can in principle, even if not in practice, write down a finite procedure involving finite (if perhaps unbounded in the accuracy you want) resources to obtain an arbitrarily-good approximation of every real number and thus they are in some sense “explicit”.

However, to me it suffers from a few drawbacks. One is that various styles of completeness do not hold – even if we apply the “constructive” restriction to the things within them. For example, the bounded monotone convergence theorem – which is something that looks really intuitive when you draw illustrations on a piece of paper – fails for the computable reals even if we require sequences to themselves be computable, in the sense that we can give an algorithm which approximates the nth term arbitrarily well. (Note that a sequence of computable numbers can itself be noncomputable, e.g. the sequence of digits, taken as real numbers, of Chaitin's Omega.)

Another problem is that we cannot computably test for equality – that is, there is no procedure that will let us decide if two arbitrary computable reals are equal, even though we have explicit procedures for computing them.

These two results seem somewhat unsatisfactory to me. To do math on the computable reals, then, we have to introduce caveats that make things seem less natural, and I don't like that. Which makes me wonder, is there some way around these difficulties, perhaps by suitably restricting the definition of “computable" or otherwise “constructibility”? For example, what if we limited our constructibility further to only be numbers and sequences computable by algorithms we can actually prove halt algorithmically? (They all have to be halting algorithms anyways, but here we are saying we should be able to prove they halt by an algorithm. That is, take a subset of all number and sequence and function and whatever other object-computing algorithms out there that is “nice and big enough for our use” but small enough that everything in it has its halting properties decidable by some algorithm which is valid on the entire set.)

Failing that, is there some other way to achieve this? Is there any notion of constructive which, while it may not be a “computer” definition but could be something else as long as it is, at least on small scales, practically realizable (so it cannot involve any mandatory infinities or anything like that), that results in a constructively-complete subset of real numbers with decidable equality relation and so over which we can do analysis? If so, what is it, and if not, what is the proof of impossibility?

• $\mathbb{R}$ is $\mathbb{Q}$ with also the limits of the sequences of rationals which are Cauchy for $|.|$. Now $\mathbb{R}_{definable}$ is simply $\mathbb{Q}$ with the limits of the definable sequences of rationals which are Cauchy for $|.|$. Hence $\mathbb{R}$ is complete, while $\mathbb{R}_{definable}$ is definable complete. Since everything you can define is definable, everything works well. en.wikipedia.org/wiki/Definable en.wikipedia.org/wiki/Definable_real_number – reuns Jun 5 '16 at 23:36
• I suspect that in constructive mathematics, the real numbers would be some sort of "pro-field", in which you have no equality checking and thus no inverses, but which is something like an inverse limit of an inverse system of fields. Compare with the ring $\mathbb{Q}\left[\left[x\right]\right]$ of formal power series: In constructive mathematics, it allows no equality checking either, but you can prove everything you want by "only looking at the first few coefficients", i.e., working in the rings $\mathbb{Q}\left[x\right]/\left(x^n\right)$, of which it is the inverse limit. – darij grinberg Oct 28 '18 at 18:01
• @darij: Neat idea! However I don't know how to implement it, that is, I don't know any inverse system of discrete fields which has the reals (well, any flavor of them) as limit. – Ingo Blechschmidt Oct 28 '18 at 21:08