[FOM] A question concerning continuous functions

[Andrej Bauer]

Arnon Avron <aa at tau.ac.il> writes:
> 2) In my opinion, the weakest point of Intuitionism, and the reason why
>    it will never be adopted by most mathematicians (even though many of
>    them adhere to the importance of constructive proofs) is that it 
>    seems to totally ignore geometric intuitions and concepts. As far as
>    I understand (and please correct me if I am wrong), intuitionists
>    have completely abandoned the original, intuitive concept of 
>    continuity in favor of (some constructive version of) the "official" 
>    definition.  They have ended up rejecting the classical theorems 
>    mentioned above which provide (in my opinion) the main evidence for 
>    accepting this identity in the first place... Let me add that this 
>    phenomenon provides (for me) another evidence that the two notions 
>    of continuity are not identical.

Permit me to correct you then :-).

First, about rejection of theorems:

the theorems you are referring to are not "rejected by intuitionists".
They have just been reformulated more carefully:


Constructive Intermediate Value Theorem:
   Let f : [a,b] --> R be a continuous function and f(a) <= y <= f(b).
   For every epsilon > 0 there exists x in [a,b] such that |f(x) - y| < epsilon.


Under additional assumptions about f it is possible to show that there
actually exists x such that f(x) = y, e.g., if f is a polynomial or a
sufficiently nice smooth function.

To get to the classical Intermediate Value Theorem we would want a
theorem claiming that every sequence in a bounded interval has a
convergent subsequence, which is constructively invalid.

Constructive Theorem:
    Every _uniformly_ continuous function f : [a,b] --> R is
    bounded. Moreover, there exists M such that f(x) <= M for
    all x in [a,b], and for every M' < M there exists x in [a,b]
    with M' < f(x) <= M. In other words, M is the supremum of f.

Again, to conclude that there is x such that f(x) = M, we would need
to know that every sequence on a closed interval has a convergent
subsequence.

It is a classical accident that every continuous function on a closed
interval is also uniformly continuous.


Second, about abonding geometric intuitions:

Intuitionistic logic is _required_ for an axiomatization of the truly
geometric intuition of "continuum" as an indivisible space containing
infinitesimals. I am referring to synthetic differential geometry.

Furthermore, when students of mathematics are presented with geometric
constructions that shatter their geometric intuitions (a function that
is differentiable precisely at all irrational numbers, Banach-Tarski
paradox, non-measurable sets, etc), these are all very heavily
classical constructions. Does this not mean that it is the fault of
classical mathematics that human geometric intuitions are in conflict
with the official truth?

Andrej Bauer
University of Ljubljana
http://andrej.com/