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?

Solution 1:

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".

Solution 2:

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.