FOM: intuitionistic mathematics and building bridges

[Stephen G Simpson]

This is a reply to Neil Tennant's posting of 9 Feb 1998 17:57:16.

Background: In my posting of 5 Feb 1998 13:46:09 I expressed doubts
about the viability of intuitionistic or constructive mathematics for
applications, since many basic theorems of calculus (e.g. every
continuous f:[0,1] -> R has a maximum) are lost.  Neil challenged
this.  I'm not sure that I understand the thrust of Neil's comment,
but basically it seems to be as follows: Even if a classical theorem S
is not intuitionistically valid, we can still get something like the
double negation, not not S, so no predictive power is lost.

I have two points to make.

First, note that Tennant's procedure is not the one that is actually
followed by Brouwer and Bishop.  For instance, Bishop doesn't propose

     not not (every continuous f:[0,1] -> R has a maximum) 

as his constructive analog of the classical calculus result.  Indeed,
the "not not" version would be pointless from Bishop's point of view.
Instead Bishop proposes another constructive analog, which is clumsier
and harder to remember, but which he prefers because of its so-called
constructive content.  My real question is whether Bishop's
formulations may not constitute an impediment to applicability.  In
order for a mathematical theorem to be applicable, it has to be simply
and elegantly stated, so that people can retain it in their minds.
Bishop tries hard, but in my opinion many of his formulations do not
meet this test of simplicity and elegance.

Second, we need to remember that the double negation transform is
purely formal does not respect philosophical motivation.  And
philosophical motivation is all-important, especially when it comes to
applications.  There is a sharp contrast here!  Classical mathematics
is motivated by some sort of realistic outlook:

  "Mathematical objects exist independently of our consciousness."

This is why the law of the excluded middle, Av~A, is classically
valid.  It is also why the classical mindset is at least sometimes in
tune with real-world applications.  The real world is a very objective
place!  By contrast, intuitionism is based on a solipsistic or
subjectivist philosophy:

  "Mathematics consists of mental constructions." 

This anti-objective outlook may not be suitable if we want to apply
our mathematics to the real world.  I believe that this is the
fundamental philosphical reason why intuitionism and constructivism
never really caught on: they are literally out of touch with reality,
hence likely to be hopeless when it comes to real-world applications.

Surely I am not the first to make this point.  But where is it in the
philosophical or f.o.m. literature?

-- Steve