To what extent can the mathematics of Reals be applied to Computable Reals?

Question

Is there a general theorem that would state, with proper sanitization, that most known results regarding the use of real numbers can actually be used when considering only computable reals? Or is there a proper characterisation of results that remain valid when considering only the computable reals? A side question is whether results concerning computable reals can be proved without having to consider all real, or anything that is not computable. I am thinking specifically of calculus and mathematical analysis, but my question is in no way limited to that.

Actually, I suppose there is a hierarchy of computable reals corresponding to the Turing hierarchy (Is that correct?). Then, more abstractedly, is there an abstract theory of real (I am not sure what the terminology should be), for which a number of results could be proved, that would apply to the traditional real numbers, but also to computable reals, and to any level of the Turing hierarchy of computable reals, if it exists.

Then my question could possibly be stated as: Is there a characterization of results that will apply in the abstract theory of reals when they have been proved for traditionnal reals. And, could these results be proved directly in the abstract theory, without considering traditional reals.

I am also interested in understanding how and when these theories of reals diverge.

P.S. I do not know where to fit this in my question. I realised that a good deal of the mathematics on the reals have been generalized with topology. So it may be that the answer to my question, or part of it, can be found there. But there may also be more to it.

Answer 1

The real numbers may be characterized in a couple of ways, let us work with the Cauchy-complete archimedean ordered field. (We need to be a bit careful how exactly we say this, see Definition 11.2.7 and Defintion 11.2.10 of the HoTT book.)

The following theorem is valid in any topos (a model of higher-order intuitionistic logic):

Theorem: There is a Cauchy-complete archimedean ordered field, and in fact any two such fields are canonically isomorphic.

Moreover, in intuitionistic logic (not to be confused with intuitionism) we can do a lot of real analysis (sequences and limits, derivatives, integrals, continuity, uniform continuity, etc.) which is then valid in any topos. If we take the topos of sets we get the usual real analysis. By taking a different topos we get a different kind of real analysis – and there is a topos which yields precisely the computable reals and computable real analysis.

This of course is the effective topos, in which the real numbers are the computable reals (speaking vaguely, the reason for this is that the effective topos is constructed in such a way that everything in it is automatically computable). The answer to your question is

Definitions, constructions, and theorems in intuitionistic real analysis are automatically translated to definitions, constructions and theorems about computable reals when we interpret them in the effective topos.

For instance, the theorem "every uniformly continuous map $f : [0,1] \to \mathbb{R}$ attains its supremum" is intuitionistically valid. When we interpret it in the effective topos we get the corresponding version for computable maps on computable reals which are computably uniformly continuous.

You also ask about the "divergence" between real analysis and its computable version. The answer is that results which rely on the law of excluded middle or the axiom of choice (although countable choice is ok) are not intuitionistic, and therefore cannot be validated in the effective topos. However, we should note that (contrary to popular opinion) most analysis can be done intuitionistically.

The effective topos is just one of many realizability toposes. When we interpret intuitionistic analysis in other realizability toposes we get alternative models of real number computatability, including computation with oracles which you allude to. The "relative Kleene function realizability topos" (whatever that is) gives the so called Type II computability on reals in which computable maps operate on all reals, not just the computable ones.

I tried to explain this once in the notes "Realizability as the Connection between Computable and Constructive Mathematics", and before that in my Ph.D. thesis.