28
$\begingroup$

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?

$\endgroup$
13
  • 3
    $\begingroup$ I don't know the setting, but characteristic functions of a point usually exists in most weak logical systems. $\endgroup$
    – William
    Jul 28, 2012 at 20:55
  • 4
    $\begingroup$ Well, all computable functions are continuous... $\endgroup$
    – user856
    Jul 28, 2012 at 21:01
  • 9
    $\begingroup$ 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. $\endgroup$
    – GEdgar
    Jul 28, 2012 at 21:04
  • $\begingroup$ 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... $\endgroup$
    – user29743
    Jul 28, 2012 at 21:09
  • 3
    $\begingroup$ @Asaf: no. In fact, the way the formalization goes, the only "functions" from $\mathbb{R}$ to $\mathbb{R}$ that can be developed at all in $\mathsf{RCA}_0$ are "coded continuous functions". $\endgroup$ Jul 28, 2012 at 21:37

4 Answers 4

33
$\begingroup$

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

$\endgroup$
12
$\begingroup$

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.

$\endgroup$
7
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$ Jul 28, 2012 at 21:34
  • $\begingroup$ @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. $\endgroup$
    – user452
    Jul 28, 2012 at 21:39
1
$\begingroup$

Here you go: http://www.andrew.cmu.edu/user/ulrikb/80-518-818/Brouwer-1927.pdf

This is a translation of Brouwer's 1927 paper which proves the bar, fan, and continuity theorems (the last one is what you want). It's actually a scan from "From Frege to Godel."

Heyting's "Intuitionism: An Introduction" found here also provides a proof in section 3.

$\endgroup$
1
  • $\begingroup$ The first link is broken. $\endgroup$
    – Shaun
    Apr 7, 2021 at 11:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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