A famous result in intuitionistic mathematics is that all real-valued total functions are continuous. Since the requirements for a function to be admitted intuitionistically is that it must define a procedure or algorithm, all functions are computable. This seems to suggest that all computable functions are continuous. My questions are:
- Is this true for all total recursive or just primitive recursive functions?
- Where can I find such a proof?
- Conversely, what are examples of continuous functions that are not computable?
By the way, I heard here and here that most intuitionistic formal systems can only prove that there are no real-valued total discontinuous functions, not the stronger positive result that all functions are continuous.
Best Answer
Basically, we might say that computable real numbers are equivalence classes of Cauchy sequences of rationals. To specify a sequence computably, you need a computable function $s$ from natural numbers to rationals. To ensure it is Cauchy, there should be another computable function $N$ such that for all $m$, if $n, n' > N(m)$ then $|s(n) - s(n')| < 1/m$.
One difficulty is that it is impossible in general to compute whether two such real numbers are equal. For example, consider the real number defined as follows. If there is no odd perfect number $k < n$, then $s_n = 0$, else $s_n = 1/k$ where $k$ is the least odd perfect number. Here we can take $N(m) = m$. This fits the definition above, so it corresponds to a computable real number, let's call it $b$. But without knowing whether there is an odd perfect number, we can't tell whether $b=0$.
Now a computable function from computable reals to computable reals has to take $s$ and $N$ above, corresponding to real number $x$, as "black boxes" and produce new functions $\tilde{s}$ and $\tilde{N}$ defining another computable real number $f(x)$. Moreover it must do it in such a way that if $s$, $N$ and $s'$, $N'$ define the same real number, $\tilde{s}$ and $\tilde{N}$ define the same real number as $\tilde{s'}$ and $\tilde{N'}$. But $\tilde{s}(n)$ and $\tilde{N}(m)$ must be obtained by finite computations, in particular only involving finitely many values of $s$ and $N$. This is the essential reason why discontinuous functions are not going to work. Suppose $f$ is discontinuous at $0$, so that for some $y < z$ there are some reals arbitrarily close to $0$ with $f$ values $\ge z$ and others $\le y$. You can't approximate $f(x)$ arbitrarily well knowing only finitely many values of $s$ and $N$: those values could be consistent with either $f(x) \le y$ or $f(x) \ge z$.