FOM: Re: building bridges with consructive analysis

[Todd Wilson]

Carsten Butz:
> Would they agree that Brouwer or Bishop would have been able to
> build a bridge?  
 
Stephen Simpson:
> I don't think this is the right question.  A better question is: Would
> Brouwer or Bishop have been able to build a bridge using
> intuitionistic or constructive mathematics?  There is a big difference
> between these two questions, [...]
>
> I have my doubts about whether intuitionistic and/or constructive
> mathematics is "enough to build bridges".

For all practical purposes (e.g., building bridges), I don't see any
real difference between classical and, say, Bishop-style constructive
mathematics.  While it is certainly true that many theorems of
classical analysis are not constructively valid as stated, most of
them have constructive substitutes that, when it comes to building
bridges, are just as good.

To take an example that has been mentioned already several times,
consider the theorem that every continuous function  f:[0,1]->R
attains a maximum value.  While it is true constructively that any
such function has a *supremum* on [0,1], one cannot always find a
particular point in [0,1] at which this supremum is attained.
However, given any e > 0, one can always find a point x in [0,1] such
that f(x) is within epsilon of this supremum.  Many other theorems of
classical analysis not constructively valid receive such "within
epsilon" substitutes.  And when what goes into building bridges is
numerical simulation and machine processes that can stand errors on
the magnitude of one millionth of an inch, one can always choose an
epsilon for which the constructive substitutes are sufficient.

Todd Wilson
Associate Professor of Computer Science
California State University, Fresno
PhD:  Pure and Applied Logic, Carnegie Mellon