# All real functions are continuous

I've heard that within the field of intuitionistic mathematics, all real functions are continuous (i.e. there are no discontinuous functions). Is there a good book where I can find a proof of this theorem?

-
I don't know the setting, but characteristic functions of a point usually exists in most weak logical systems. – William Jul 28 '12 at 20:55
– Rahul Jul 28 '12 at 21:01
But, intuitionistically: Given a real you may not be able to tell whether it is equal to that point. So "characteristic function of a point" is not a "function" in the sense they use over there in Intuitionism Land. – GEdgar Jul 28 '12 at 21:04
I saw a proof in a (leisurely) intro to philosophy of mathematics book for undergraduates, which I remember was blue, but I don't remember the author... – user29743 Jul 28 '12 at 21:09
@RahulNarain Computable functions are usually function on the natural numbers to natural numbers. I am not aware of any definition of computable real value functions. – William Jul 28 '12 at 21:17

Brouwer proved (to his own satisfaction) that every function from $\mathbb{R}$ to $\mathbb{R}$ is continuous. Modern constructive systems rarely are able to prove this, but they are consistent with it - they are unable to disprove it. These system are also (almost always) consistent with classical mathematics in which there are plenty of discontinuous functions from $\mathbb{R}$ to $\mathbb{R}$. One place you can find something about this is the classic Varieties of Constructive Mathematics by Bridges and Richman.

The same phenomenon occurs in classical computable analysis, by the way. Any computable function $f$ from $\mathbb{R}$ to $\mathbb{R}$ which is well defined with respect to equality of reals (and thus is a function from $\mathbb{R}$ to $\mathbb{R}$ in the normal sense) is continuous. In particular the characteristic function of a singleton real is never computable. This would be covered in any computable analysis text, such as the one by Weihrauch.

Here is a very informal argument that has a grain of truth. It should appear naively correct that if you can "constructively" prove that something is a function from $\mathbb{R}$ to $\mathbb{R}$, then you can compute that function. So the classical fact that every computable real function is continuous suggests that anything that you can constructively prove to be a real function will also be continuous. This suggests that you cannot prove constructively that any classically discontinuous function is actually a function. The grain of truth is that there are ways of making this argument rigorous, such as the method of "realizability".

-

There exists a Grothendieck topos $\mathcal{E}$ in which the statement "every function from the Dedekind real numbers to the Dedekind real numbers is continuous" is true in the internal logic. To be a little more precise, in the topos $\mathcal{E}$, there is an object $R$ of Dedekind cuts of rational numbers, such that $$\forall f \in R^R . \, \forall \epsilon \in R . \, \forall x \in R . \, \epsilon > 0 \Rightarrow \exists \delta \in R . \, \forall x' \in R . \, \left| x - x' \right| < \delta \Rightarrow \left| f (x) - f (x') \right| < \epsilon$$ holds when interpreted using Kripke–Joyal semantics in $\mathcal{E}$. The topos $\mathcal{E}$ is constructed as follows: we take a full subcategory $\mathbb{T}$ of the category of topological spaces $\textbf{Top}$ such that

• $\mathbb{T}$ is small,
• the real line $\mathbb{R}$ is in $\mathbb{T}$,
• for each $X \in \operatorname{ob} \mathbb{T}$ and each open subset $U$ of $X$, we have $U \in \operatorname{ob} \mathbb{T}$, and
• $\mathbb{T}$ is closed under finite products in $\textbf{Top}$;

and we set $\mathcal{E}$ to be the category of sheaves on $\mathbb{T}$ equipped with the open immersion topology. One can then show that the object of internal Dedekind real numbers in $\mathcal{E}$ is (isomorphic to) the representable sheaf $\mathbb{T}(-, \mathbb{R})$, and with more work, one finds that Brouwer's "theorem" holds in $\mathcal{E}$. The details of the construction and the proof of validity can be found in [Sheaves in geometry and logic, Ch. VI, §9], though I have not understood it in full.

-

Real Analysis: A Constructive Approach (2007) by Mark Bridger will have what you want. On Part 157 of my copy, Chapter 4 Appendix 1 is "Are There Non-Continuous Functions", and the answer is none that can be constructed on a finite closed interval. Under the intuitionist logic used in this book, step functions and the like cannot be defined on finite closed intervals, because say for a function $f(x)$ with a discontinuity at $0$, you cannot say precisely whether $x<0$, $x=0$, or $x>0$ (as Carl Mummert notes in his comment and answer). Yes, I think that's weird, but that's how some intuitionist logic works.

-
I don't know Bridger's book. Is Bridger's system actually strong enough to prove that every function is continuous, or is it just not strong enough to prove that there is a discontinuous function? Most constructive systems, like Bishop's, have only axioms that are classically true, and thus follow the latter pattern. – Carl Mummert Jul 28 '12 at 21:34
@Caarl Mummert: No, what I said was too strong, and I edited the answer. Bridger is following Bishop, and he makes clear that he is talking about functions defined at every point on a finite closed interval. – trb456 Jul 28 '12 at 21:39
Thanks, that answers my question! – Carl Mummert Jul 28 '12 at 21:40