<p>The real numbers may be characterized in a couple of ways, let us work with <strong>the Cauchy-complete archimedean ordered field</strong>. (We need to be a bit careful how exactly we say this, see <a href="http://books.google.si/books?id=LkDUKMv3yp0C&amp;lpg=PP1&amp;dq=homotopy%20type%20theory&amp;pg=PA372#v=onepage&amp;q&amp;f=false">Definition 11.2.7</a> and <a href="http://books.google.si/books?id=LkDUKMv3yp0C&amp;lpg=PP1&amp;dq=homotopy%20type%20theory&amp;pg=PA373#v=onepage&amp;q&amp;f=false">Defintion 11.2.10</a> of the <a href="http://homotopytypetheory.org/book/">HoTT book</a>.)</p>

<p>The following theorem is valid in any <a href="http://ncatlab.org/nlab/show/topos">topos</a> (a model of higher-order intuitionistic logic):</p>

<blockquote>
  <p><strong>Theorem:</strong> There is a Cauchy-complete archimedean ordered field, and in fact any two such fields are canonically isomorphic.</p>
</blockquote>

<p>Moreover, in <a href="http://ncatlab.org/nlab/show/intuitionistic+logic">intuitionistic logic</a> (not to be confused with <a href="http://en.wikipedia.org/wiki/Intuitionism">intuitionism</a>) 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.</p>

<p>This of course is the <a href="http://ncatlab.org/nlab/show/effective+topos">effective topos</a>, in which the real numbers <em>are</em> 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</p>

<blockquote>
  <p><em>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.</em></p>
</blockquote>

<p>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. </p>

<p>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) <em>most</em> analysis can be done intuitionistically.</p>

<p>The effective topos is just one of many <a href="http://ncatlab.org/nlab/show/realizability+topos">realizability toposes</a>. 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 <a href="http://ncatlab.org/nlab/show/Type+Two+Theory+of+Effectivity">Type II computability</a> on reals in which computable maps operate on <em>all</em> reals, not just the computable ones.</p>

<p>I tried to explain this once in the notes <a href="http://math.andrej.com/2005/08/23/realizability-as-the-connection-between-computable-and-constructive-mathematics/">"Realizability as the Connection between Computable and Constructive Mathematics"</a>, and before that in my <a href="http://andrej.com/thesis/">Ph.D. thesis</a>.</p>

CC BY-SA 3.0
2014-08-12T19:47:12.077Z
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
CC BY-SA 3.0
2014-08-12T19:49:51.357Z
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
CC BY-SA 3.0
2014-08-12T19:50:55.317Z
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
CC BY-SA 3.0
2014-08-12T19:53:24.190Z
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
CC BY-SA 3.0
2014-08-12T20:13:22.460Z
So, I'm remembering my Constructive Analysis (Bishop and Bridges), and the Constructive reals described there sure seemed like the computable reals.  In it, it was noted that every theorem of real analysis was true in their constructive analysis with a pair of nots at the front?  It has been a while.
Yakk
CC BY-SA 3.0
2014-08-12T23:05:14.853Z
@Yakk, that is the general idea behind Bishop style constructivism: if we change the statement of a classical theorem such that the required information is given more explicitly we can _often_ obtain a restatement that is true both constructively and classically. But it is not a meta-theorem, rather a guideline. What Andrej is saying is a meta-theorem: if you only use constructive logic (but no axioms which are not true in all topoi) then the theorem is true in all topoi: classical analysis is the topos of sets, and there are various computable topoi, and the result holds in all of them.
Kaveh
CC BY-SA 3.0
2014-08-13T07:09:27.723Z
It's a bit of an oxymoron to say "true both constructively and classically". That's like saying I have "more than 50 and more than 30 euros in my pocket" -- remember that *constructive implies classical*.
Andrej Bauer
CC BY-SA 3.0
2014-08-13T07:10:49.613Z
@Yakk: Bishop's definition of reals never mentions any "computability". He may talk about it in the accompanying text, but the definition is "just math":  real is represented by a sequence $(a_n)_n$ of rational numbers such that $|a_n - a_m| < 1/n + 1/m$ for all $n, m$. The word "computable" does not appear, nor is it implied.
Andrej Bauer
CC BY-SA 3.0
2014-08-13T13:42:33.780Z
I am using "constructive" in a more general sense, not just logic, i.e. in the sense used by Troelstra in his [article](http://staff.science.uva.nl/~anne/hhhist.pdf).
Kaveh
CC BY-SA 3.0
2014-08-13T14:15:43.547Z
@Kaveh: yeah, we could wish for better terminology...
Andrej Bauer
CC BY-SA 3.0
2014-08-12T15:31:11.403Z
2014-08-12T19:52:54.070Z
2014-08-12T19:52:54.070Z
Andrej Bauer
<p>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.</p>

<p>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.</p>

<p>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.</p>

<p>I am also interested in understanding how and when these theories of
reals diverge.</p>

<p>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.</p>

<computability><computing-over-reals><topology><model-theory>
To what extent can the mathematics of Reals be applied to Computable Reals?
babou
# To what extent can the mathematics of Reals be applied to Computable Reals?

(Asked by: username_0 on 2014-08-12)

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.

**Tags:** computability, computing-over-reals, topology, model-theory


---

## 1 answers

### Answer by username_1 on 2014-08-12. Score: 16 | Accepted answer

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](http://books.google.si/books?id=LkDUKMv3yp0C&lpg=PP1&dq=homotopy%20type%20theory&pg=PA372#v=onepage&q&f=false) and [Defintion 11.2.10](http://books.google.si/books?id=LkDUKMv3yp0C&lpg=PP1&dq=homotopy%20type%20theory&pg=PA373#v=onepage&q&f=false) of the [HoTT book](http://homotopytypetheory.org/book/).)

The following theorem is valid in any [topos](http://ncatlab.org/nlab/show/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](http://ncatlab.org/nlab/show/intuitionistic+logic) (not to be confused with [intuitionism](http://en.wikipedia.org/wiki/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](http://ncatlab.org/nlab/show/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](http://ncatlab.org/nlab/show/realizability+topos). 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](http://ncatlab.org/nlab/show/Type+Two+Theory+of+Effectivity) 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"](http://math.andrej.com/2005/08/23/realizability-as-the-connection-between-computable-and-constructive-mathematics/), and before that in my [Ph.D. thesis](http://andrej.com/thesis/).

> **Comments:**
> **username_2**: 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?  
> **username_1**: 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.  
> **username_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.  
> **username_1**: 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.  
> **username_3**: So, I'm remembering my Constructive Analysis (Bishop and Bridges), and the Constructive reals described there sure seemed like the computable reals.  In it, it was noted that every theorem of real analysis was true in their constructive analysis with a pair of nots at the front?  It has been a while.  
> **username_4**: @username_3, that is the general idea behind Bishop style constructivism: if we change the statement of a classical theorem such that the required information is given more explicitly we can _often_ obtain a restatement that is true both constructively and classically. But it is not a meta-theorem, rather a guideline. What Andrej is saying is a meta-theorem: if you only use constructive logic (but no axioms which are not true in all topoi) then the theorem is true in all topoi: classical analysis is the topos of sets, and there are various computable topoi, and the result holds in all of them.  
> **username_1**: It's a bit of an oxymoron to say "true both constructively and classically". That's like saying I have "more than 50 and more than 30 euros in my pocket" -- remember that *constructive implies classical*.  
> **username_1**: @username_3: Bishop's definition of reals never mentions any "computability". He may talk about it in the accompanying text, but the definition is "just math":  real is represented by a sequence $(a_n)_n$ of rational numbers such that $|a_n - a_m| < 1/n + 1/m$ for all $n, m$. The word "computable" does not appear, nor is it implied.  
> **username_4**: I am using "constructive" in a more general sense, not just logic, i.e. in the sense used by Troelstra in his [article](http://staff.science.uva.nl/~anne/hhhist.pdf).  
> **username_1**: @username_4: yeah, we could wish for better terminology...  

---

