FOM: science and constructive mathematics

[Peter Schuster]

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. 

Peter Schuster.