FOM: science and constructive mathematics

[Matthew Frank]

Some comments on the posts by Tennant and Schuster:

(Bibliographic comment:  A week ago, I put on my web page a paper titled
"Constructive Mathematics and Mathematical Physics:  A Program and
Progress Report".  This is a companion to my paper on "Constructive Math:
Why and How", which I put on that web page and mentioned on this list a
month ago.  Tennant's post is, in part, a response to the newer paper.)

In my paper, I discuss a local strategy of constructivizing various
results of mathematical physics; Tennant proposed an alternative global
strategy (more or less via double negation).  But these two strategies
have two very different goals.  Tennant's goal is to show that, under
certain construals of science, "one does not *need* anything more than
constructive reasoning in order to 'do science'."  My goal is to show the
worthwhileness of the pursuit of constructive mathematics, and
constructive treatments of mathematical physics in particular.  I doubt
that either strategy helps much towards the other goal.

(A side note:  I don't think it makes sense to cast the issue as entirely
one of logic, as Tennant's argument does.  For instance, if one develops
one's mathematical physics in ZFC, then one does not need the principle of
the excluded middle because ZFC (under most formulations of the axiom of
choice) under intuitionist logic proves every instance of excluded middle
in the language of set theory.  This is truly a trivial sense of the
dispensability of classical logic.)

Schuster says "my impression is that if there is any constructive proof of
some theorem then one can find it in a rather direct way as soon as one
has put the concepts right".  From personal experience, I disagree--
putting the concepts right is often the most interesting and most valuable
part of the proof, but it does not always make the rest trivial or easy.

Schuster also argued for constructive mathematics on the grounds that
"dropping axioms (excluded middle, commutativity) yields a more general
theory that is wider open for applications, even if now one cannot dream
of some of them."  If (in some bizarre counterfactual sense) we hadn't
dreamed of non-abelian groups, I doubt that non-abelian group theory would
be worthwhile.  So I do not think this a particularly good argument for
Bishop-style constructive mathematics.  My argument (in the "Why and How"
paper) is that constructive mathematics gives us a different perpsective
on mathematics, and therefore a source of insight--perhaps I should have
said that I reject most of the other arguments that have been given for
it.

--Matt
http://www.math.uchicago.edu/~mfrank