FOM: Re: science and constructive mathematics

[Neil Tennant]

Peter Schuster writes:

> Let me first give a brief summary of how one could understand 
> Neil Tennant's posting, who might forgive me any misinterpretation.  

Will do (i.e. forgive).
 
> (1) The mathematics which is needed in natural science, for falsifying 
> hypotheses, consists mainly of negative statements. 

This is a little vague. How about: the (classical) mathematics that some
might claim is "needed" for natural science can, by classical lights, all
be expressed in a language without the universal quantifier. (Use the
equivalence "for x F(x) iff not-some x-not-F(x)".)
 
> (2) Each "for-all" statement can be rephrased without loss 
> of content as a "there-is-none-such-that-not" statement. 

Yes; without loss of would-be *classical* content.

> (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. 

Yes.

> (5) Constructive proofs are much less feasible than traditional ones. 

Better to put it another way: using classical methods (e.g. proving P by
refuting not-P) often gives us much shorter proofs than any known
constructive proof of the same result.
 
> (6) By (4), mathematics as applied in science does not have to be developed 
> in any constructive setting, since it is constructive anyway. 

I'd put it another way: Whatever mathematical theorems are applied in
science, the overall chain of reasoning (from mathematical axioms and
scientific hypotheses to predictions) *can in principle  be 
constructivized if necessary*. Note that the overall chain of reasoning
would involved certain mathematical theorems as cut points. The cut-free
derivation might well not contain those theorems at all!

> In particular, 
> one  may stick to traditional methods, and one might better do so for, by (5), 
> they are the more efficient ones.

Yes, with "might well be" substituted for "are".

> 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. 

I think this gets the dialectic wrong. I am trying to argue (like you) on
behalf of the constructivist. Our opponent, the classicist, is trying to
insist that classical logic (and mathematics) is both correct and *needed*
for applications in science. To counter this, I say to the opponent
"Choose such-and-such forms of expression for your classically construed
claims (i.e. the forms lacking universal quantifiers.)" Our classical
opponent agrees, by his lights, to do this, thinking that it cannot matter
one way or the other which form of expression is employed, provided only
that it is *classically* equivalent to whatever canonical form might
otherwise be used. Then I say to him "Your application of [classical]
logic in the derivation of testable (and decidable) predictions turns out
to be unnecessary; intuitionistic reasoning will suffice."  (In fact,
intuitionistic *relevant* reasoning will suffice!)
 
> Secondly, I cannot entirely subscribe to (1), (4), and (5). Is it really true that 
> scientist only want falsification? 

No; they want predictions, in general. But predictions are always
decidable statements; so my point about the sufficiency of constructive 
logic can be sustained.

> 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. 

Agreed; and this would be more grist to the mill in favor of
intuitionistic logic. IL *suffices* for all the mathematics applied in
science; and restricting oneself to IL might provide more useful
information, as you point out. Against this, the use of CL might lead to
our obtaining an applicable result [i.e.: mathematical theorem] whose 
proof in IL might be very difficult to come by, if not impossible. But
because of the way that the theorem in question functions as a *cut
sentence* within the hypothetico-deduction involved, it would "disappear"
in the process of cut-elimination and constructivization of the overall
reasoning conducted, in the language free of the universal quantifier, to
the prediction from the mathematical *axioms* plus the scientific
hypotheses.

> 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. 

The phenomenon of being able more easily to find a constructive proof
(because of the constructive meanings of the operators) has to be
reconciled with the (possibly counterintuitive) fact that the complexity
of the decision problem for intuitionistic [relevant] propositional logic
is worse than that of classical propositional logic (PSPACE-complete v.
NP-complete, respectively). And at first-order, IL is undecidable with
just two monadic predicates, whereas CL becomes undecidable only upon the
addition of a two-place predicate. But these worst-case complexity
comparisons might turn out to be of slender relevance to the kind of
logical reasoning involved in finding scientifically applicable
mathematical theorems.

Neil Tennant