FOM: science and constructive mathematics
pschust at rz.mathematik.uni-muenchen.de
Mon Jun 19 10:22:26 EDT 2000
Late reply to
>Date: Wed, 14 Jun 2000 13:02:13 -0400 (EDT)
>From: Neil Tennant <neilt at mercutio.cohums.ohio-state.edu>
Let me first give a brief summary of how one could understand
Neil Tennant's posting, who might forgive me any misinterpretation.
(1) The mathematics which is needed in natural science, for falsifying
hypotheses, consists mainly of negative statements.
(2) Each "for-all" statement can be rephrased without loss
of content as a "there-is-none-such-that-not" statement.
(3) By metamathematics, intuitionistic logic is just as good as classical logic
for proving negative statements without universal quantifiers.
(4) By (1-3), constructive mathematics is just as powerful as traditional
mathematics for doing natural science.
(5) Constructive proofs are much less feasible than traditional ones.
(6) By (4), mathematics as applied in science does not have to be developed
in any constructive setting, since it is constructive anyway. In particular,
one may stick to traditional methods, and one might better do so for, by (5),
they are the more efficient ones.
My remarks to all this are as follows.
First, how to interpret "for all x P(x)" obviously becomes a crucial point when
one leaves the realm of classical logic, in particular, when x ranges over some
infinite set. Identifying this with "there is no x such that not P(x)" requires,
however, that P(x) can be proven, for any given x, by deriving a contradiction
from the assumption not P(x). To this end, one has to use reductio ad absurdum,
unless P(x) is properly decidable for each x; in other words, classical logic
has to be built in from the outset, unless all observable properties in science
are decidable what they presumably are not.
Secondly, I cannot entirely subscribe to (1), (4), and (5). Is it really true that
scientist only want falsification? Although most of them don't seem to care about
which mathematics/logic one uses to get the desired theorems, they might well want computational content, mathematical witnesses, algorithms, programs, and so on; and all this lies close to the heart of constructive mathematics. If only in this
sense, constructive mathematics could provide better mathematics also for
scientific applications. Moreover, who knows whether reality(!) obeyes tertium non
datur? The case is just as for noncommutative algebra/geometry which indeed
provides a better framework for some physical theories: 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. Last but not
least, I am very reluctant to accept something like (5): besides the fact
that constructive proofs are much more suitable for being generated and for
being checked by machine-assistance, they are more straightforward even for
human thinking (ask some first-year students!): there are no indirect
arguments, only clear distinctions-by-cases, etc.. Someone else might know
better about the proof-theoretic complexity of constructive vs. classical proofs;
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.
More information about the FOM