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?

Solution 1:

You might like the field of algebraic real numbers (or algebraic complex numbers), that is, those numbers which happen to be the solution of some polynomial equation with rational coefficients.

Equality on algebraic numbers can be shown, without the law of excluded middle and without any form of choice, to be decidable. And indeed, there is an algorithm which, given two algebraic numbers (as oracles which can be queried for better and better rational approximations, together with polynomial equations they are solutions of) determines whether the numbers are equal or apart from each other. In the latter case it even outputs a (positive) lower bound on their distance.

Edit. A reference is A Course in Constructive Algebra by Mines, Richman and Ruitenburg (Chapter VI.1). Theorem 1.9 there contains a general result regarding algebraic numbers over discrete fields. A direct proof just for the algebraic real or complex numbers appears as Proposition 1.6 of this book draft (in German). If there's interest I'll write down a translation of the short proof. There are surely further places where this is written down; it's part of the standard constructive folklore.