Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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.

share|improve this question

1 Answer 1

up vote 15 down vote accepted

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.

share|improve this answer
    
I am confused about something then. I recall that the Heine-Borel theorem (that the interval $[0,1]$ is compact) fails for the computable reals, yet is valid intuitionistically. Am I misrecalling something, or is this a matter of definitions, or something else? –  Joshua Grochow Aug 12 at 19:47
3  
No, no, you need to distinguish between intuitionistic logic and Brower's intuitionism. Brouwer's intuitionism has extra axioms which imply that $[0,1]$ is Heine-Borel compact. Intutionistic logic is just classical logic without excluded middle (and no extra axioms), so it is compatible with classical logic. In intuitionistic logic we can show that $[0,1]$ is complete and totally bounded as a metric space, which is another kind of compactness. But we cannot show intuitionistically that $[0,1]$ is Heine-Borel compact. –  Andrej Bauer Aug 12 at 19:49
1  
If you want $[0,1]$ to be Heine-Borel compact you should use Type Two Computability, i.e., the relative Kleene function realizability. There $[0,1]$ is computably Heine-Borel compact. –  Andrej Bauer Aug 12 at 19:50
    
I added a note to about the fact that intuitionistic logic is not the same thing as intuitionism. Also, the Wikipedia page on intuitionistic logic is awful. –  Andrej Bauer Aug 12 at 19:53
1  
@Kaveh: yeah, we could wish for better terminology... –  Andrej Bauer Aug 13 at 14:15

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.