18
$\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?

  • 3
    I don't know the setting, but characteristic functions of a point usually exists in most weak logical systems.2012-07-28
  • 3
    Well, [all *computable* functions are continuous](http://blog.sigfpe.com/2008/01/what-does-topology-have-to-do-with.html)...2012-07-28
  • 5
    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.2012-07-28
  • 0
    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...2012-07-28
  • 0
    @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.2012-07-28
  • 0
    Most weak logical systems are not able to form the characteristic function of a singleton real. This includes not only constructive systems but weak classical systems such as the system $\mathsf{RCA}_0$ used in reverse mathematics.2012-07-28
  • 0
    @Carl: But I suppose that $\mathsf{RCA}_0$ can still form the characteristics function of $\{0\}$, or maybe even $\mathbb{N,Z}$ or $\mathbb Q$? None of those are continuous [everywhere].2012-07-28
  • 2
    @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".2012-07-28
  • 0
    @CarlMummert What exactly is a function from the real to the reals in second order arithmetics. Simpson does something about functions between separable metric spaces. It require some coding, but it seems to only capture the continuous functions.2012-07-28
  • 0
    @William: exactly, it only captures continuous functions. In that context a continuous function is coded by a set of neighborhood conditions, and a function from $\mathbb{R}$ to $\mathbb{R}$ is just a special case of a function between two complete separable metric spaces.2012-07-28
  • 0
    @William: The blog post I linked to defines a real number as a Cauchy sequence of rationals with certain conditions on the rate of convergence, and considers functions between them. But I'll defer to the people with references to actual textbooks.2012-07-28
  • 0
    You may be interested in Bell, A primer of infinitesimal analysis.2012-07-29
  • 0
    A translation of Brouwer's original paper can be found in van Heijenoort's *From Frege to Gödel: a source book in mathematical logic, 1879-1931* http://books.google.com/books/about/From_Frege_to_G%C3%B6del.html?id=q7Q-AAAAIAAJ2012-07-29

4 Answers 4

24

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

10

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.

6

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.

  • 0
    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.2012-07-28
  • 0
    @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.2012-07-28
0

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.