[FOM] Classical logic and the mathematical practice

[Andrej Bauer]

Originally constructive mathematics was indeed motivated by
philosophical reasons. But let us not forget that philosophical,
psychological, or sociological conviction is not anymore a necessary
motivation for working in constructive mathematics.

Today a mathematician may choose to work with constructive mathematics
because it is the more suitable environment for what he wants to do.
Constructive mathematics allows for _more_ possibilities than classical
mathematics. The passage from classical to constructive mathematics is
like passing from commutative to non-commutative algebra, and not like
passing from heaven to hell, contrary to a popular belief.

To name just two essential applications of constructive mathematics:

1) Synthetic Differential Geometry
   If one wants to axiomatize nilpotent infinitesimals (the ones
   that Kepler, Newton, and others used) one quickly shows that
   they do not exist, if one uses classical logic that is.
   But in intuitionistic logic a perfectly nice axiomatization is
   possible. I do not understand why this isn't taught to
   physicsts instead of the delta-epsilon analysis, which they
   forget as quickly as they can (for good reasons, too).

2) Synthetic Domain Theory
   In semantics of programming languages one wishes there were strange
   sets, e.g., a non-trivial set D that is isomorphic to the set of
   functions D->D, which can only exist in an intuitionistic world.

And more are on their way!

So as long as you're willing to mingle with computer scientists instead
of classical mathematicians, you'll be just fine doing constructive
mathematics. Not to mention it'll be easier to get funding that way.

Best regards,

Andrej Bauer