[FOM] constructive analysis

[Harvey Friedman]

On May 12, 2009, at 6:29 AM, Arnon Avron wrote:
>
>   In his Book "Mathematics: Form and function" Mac-Lane
> says somewhere that one of the main shortcomings of intuitionistic
> mathematics is that it ignores geometric intuitions (I am
> relying on my memory here, I do not have a copy of the book).
> I fully agree. Thus geometric intuitions dictate that the mean-value
> theorem (if f(0)<0 and f(1)>0 then f(a)=0 for some a in [0,1])
> should be valid for any adequate notion of a "continuous function"
> (i.e. a notion which has pretensions to correspond to
> the idea of a function whose graph can be drawn with a pencil
> without leaving the paper). As far as I know, this theorem fails
> for the constructive theory of the reals (and continuous
> functions on them). If so, then the constructive R^2 (whatever
> it is) is even less entitled to be identified with the
> true Euclidean plane than the R^2 of classical set theory.
>
>

Perhaps MacLane's comment is misleading. If we consider only uniformly  
continuous functions from [0,1] into [0,1], and use the axiom of choice

(forall n)(therexists m)(phi(n,m))) implies (therexists f)(forall n) 
(phi(n,fn))

then the intermediate value theorem is provable, constructively.

The existence of a maximum value cannot be proved in this setup.  
However, if we place conditions of "geometric understandability" on f,  
then we can prove the existence of a maximum value. E.g.,

1. x < y implies f(x) < f(y) or f(y) < f(x).
2. if x < y < z and f(x) > f(y), then f(y) > f(z).

In Reverse Mathematics (in the usual, classical sense), the existence  
of a maximum value of uniformly continuous functions is equivalent to  
WKL0 over RCA0. However, under such hypotheses, it is provable in RCA0.

Harvey Friedman