FOM: Re: your papers on constructive math

[Neil Tennant]

Matt,

I read both your papers this morning, and much enjoyed them. (I'm
referring to the first two in the list on your website).
You ought, by the way, to have your name on them as the author!
Also, be aware of posting stuff on the web in html format, if you don't
want to have your ideas stolen by unscrupulous operators.

The whole question of constructivity in physics (and the rest of science)
can, it seems to me, be approached from a more global methodological
perspective. Your local strategy is to constructivize various results as
needed. But what about the following argument? (This was first put forward
in my BJPS paper "Minimal logic is adequate for Popperian Science"
(1984), and in my book Anti-realism and Logic, OUP 1987.)

In all scientific applications, mathematical theorems (the ones that `get
applied') are *cut sentences*. First there is the mathematical proof of
the theorem, strictly within mathematics, of a sequent that we can write
as

	Axioms : Theorem

When such a theorem finds application within science, it is used, in
conjunction with scientific hypotheses, auxiliary assumptions, boundary
conditions and initial conditions, to make a prediction (or retrodiction).
Thus, using obvious abbreviations, there is a proof of a sequent of the
form

	Theorem, SHs, AAs, BCs, ICs : Prediction

We run an experiment to test the SHs---that is, we rig our apparatus so
that the BCs and ICs hold, and, so we assume, the AAs hold also. We
observe and measure the results: the Observations. If there is sufficient
discrepancy between Prediction and Observations, we have Absurdity:

	Prediction, Observations : emptyset

Now of course all this has to be put together using Cut on Theorem, and
Cut on Prediction:

Axioms : Theorem   Theorem, SHs, AAs, BCs, ICs : Prediction
____________________________________________________________cut
	Axioms, SHs, AAs, BCs, ICs : Prediction
				     Prediction, Observations : emptyset

     cut________________________________________________________________
		Axioms, SHs, AAs, BCs, ICs, Observations : emptyset

This last sequent tells us that our observations refute our scientific
hypotheses, given the truth of our mathematical *axioms* (not: theorems),
the AAs, BSs, and ICs.  (Of course, we now have to address the Quine-Duhem
problem of what to give up. If we're surer about the latter, then the SHs
will be rejected.)

Thus the applicable *theorems* of mathematics are needed only as deductive
halfway-houses on the way to refutations of scientific theories modulo the
*axioms* of mathematics.

Two more moves, and we're home. Note that for the classicist, it doesn't
matter if you write "every F is G" as "no F is not G" (in fact, in a
famous essay Popper urged that all universal hypotheses be understood as
the denial of the existence of counterexamples). Thus there is no need for
the universal quantifier anywhere in the picture above.

Secondly, note that logic is being used only to derive (ultimately) a
contradiction---i.e., a sequent whose succedent is emptyset. The
G"odel-Glivenko theorem says that any classicaly inconsistent set of
sentences (not involving the universal quantifier) is intuitionistically
inconsistent.

Thus, provided a constructive mathematician can accept the
existential-quantifiers-only version of the *axioms* (or at least, *some*
such version that is *classically* equivalent to any acceptable version),
he is free to claim, quite generally, that one does not *need* anything
more than constructive reasoning in order to "do science".

Back-up point: (virtually?) every testable prediction is *decidable*.
Hence intuitionistic logic will match classical logic in the generation of
testable predictions.

This way of seeing things also provides an explanation of why,
nevertheless, mathematicians (and scientists) are worried about forsaking
classical methods (i.e. not being able to "help themselves to" strictly
classical mathematical theorems). Because those theorems are cut-formulae
as pointed out above, they will---when judiciously chosen---effect a huge
reduction in deductive work. Any intuitionistic proof of the final sequent
that results from those two applications of cut above will, in all
probability, be horrendously, if not unfeasibly, long. So it *pays* to
work classically, especially when the applicable and net effect of doing
so is underwritten by a guarantee that, in principle, it could all be done
constructively.

Best,
Neil

PS Having written this, it seems it might be interesting to others on fom,
so I'll send fom a copy. That way too, others might have their interest
provoked in reading your two papers.
 
___________________________________________________________________
Neil W. Tennant
Professor of Philosophy and Adjunct Professor of Cognitive Science
230 North Oval
The Ohio State University