FOM: intuitionistic mathematics and building bridges

[Neil Tennant]

Steve Simpson wrote:

 > Tennant's procedure is not the one that is actually
 > followed by Brouwer and Bishop.  For instance, Bishop doesn't propose
 > 
 >      not not (every continuous f:[0,1] -> R has a maximum) 
 > 
 > as his constructive analog of the classical calculus result.  Indeed,
 > the "not not" version would be pointless from Bishop's point of view.
 > Instead Bishop proposes another constructive analog, which is clumsier
 > and harder to remember, but which he prefers because of its so-called
 > constructive content.  My real question is whether Bishop's
 > formulations may not constitute an impediment to applicability.  In
 > order for a mathematical theorem to be applicable, it has to be simply
 > and elegantly stated, so that people can retain it in their minds.

My `procedure' was not intended to emulate what the classical
applied mathematician and physicist does as far as the *mathematics*
is concerned. Rather, I wanted to make clear that the net effect of that
classical mathematics, in application within physical theorizing, can
be recovered using only intuitionistic logic, from the `same' mathematical 
*axioms*.  I explicitly pointed out that the intuitionistic proofs whose
existence was guaranteed might not even involve sentences corresponding
to the mathematical theorems being applied.  When you have a refutation of

{Mathematical axioms, Scientific hypotheses, Auxiliary assumptions,
Initial/Boundary Conditions, Observation statements}

in normal form (i.e. with no cuts) then the erstwhile mathematical theorems
being `applied' as lemmata within the overall reductio:

Mathematical axioms, 
	:	      conclusion of math. proof, premiss for applied proof
     math. proof      /
	:	     /
Mathematical theorem, Scientific hypotheses, Auxiliary assumptions,
			Initial/Boundary Conditions
		      :
		 applied proof
		      :
		Predictions, Observation statements
			    :
			Contradiction


could well have been `normalized away'.  The resulting irony would be that
one did not really `need' the mathematical theorem for the refutation of
the scientific theory.
	But of course those theorems that can be applied again and again
deserve to be available `off the shelf' for use as premisses in applied
proofs.  This is why we value the rule of cut so highly.  I think it is also
why we do classical mathematics for applications!
	The point remains, however, that any classical refutation can be
matched by an intuitionistic refutation. So in some interesting epistemological
sense one does not *in principle* NEED classical mathematics to do physics.
Intuitionistic logic working on the same axioms will yield all the needed
refutations. (Whether those axioms would be acceptable as statements of
intuitionistic mathematics is a further question.)
	I first published these observations in 1985 in the BJPS, with the
title `Minimal logic is adequate for Popperian science'. Actually, the
system of intuitionistic relevant logic is adequate also. The article
was in pointed reply to a pair of claims made be Popper:  
(i) one should interpret any scientific generality "All Fs are Gs" as 
~~Ex(Fx&~Gx); and 
(ii) one should use classical logic, since it provides the strongest 
test of one's theory against the evidence.
	Since Popperian testing is no more than the derivation of
contradictions ("between theory and evidence") it is important to note
that the weaker logical systems *match* classical logic in this regard.
Especially nice also was Popper's eschewal of the universal quantifier.
For, in its absence, we don't have to worry about inserting double negations
immediately after any universal quantifier occurrence. One then has the
straightforward metatheorem

	If X is classically inconsistent then X is inconsistent according
	to minimal (or intuitionistic relevant) logic.

This holds for the first-order language based on ~, v, &, ->, E and =.
Thus, using Popper's (i), one can refute his (ii).

Steve went on to say

 > Classical mathematics
 > is motivated by some sort of realistic outlook:
 > 
 >   "Mathematical objects exist independently of our consciousness."
 > 
 > This is why the law of the excluded middle, Av~A, is classically
 > valid.  It is also why the classical mindset is at least sometimes in
 > tune with real-world applications.  The real world is a very objective
 > place!  By contrast, intuitionism is based on a solipsistic or
 > subjectivist philosophy:
 > 
 >   "Mathematics consists of mental constructions." 
 > 
 > This anti-objective outlook may not be suitable if we want to apply
 > our mathematics to the real world.  I believe that this is the
 > fundamental philosphical reason why intuitionism and constructivism
 > never really caught on: they are literally out of touch with reality,
 > hence likely to be hopeless when it comes to real-world applications.
 > 
 > Surely I am not the first to make this point.  But where is it in the
 > philosophical or f.o.m. literature?

I don't agree with Steve that intuitionism has to be based on solipsistic
or subjectivist philosophy.  The whole interest in Dummett's meaning-
theoretic justification of intuitionism is that it gets away from the
earlier solipsistic motivation that Brouwer had. Dummett's argument for
intuitionism is based, rather, on the *publicity* of communication, and
the so-called Manifestation Requirement. The MR is that grasp of meaning
should be able to be made manifest in the appropriate exercise of recognitional
capacities relating to the use of sentences. Moreover, the intuitionist is
demanding a very great degree of objectivity for mathematical claims---namely,
possession of a proof! If any semantics is objectivist, it is intuitionistic
semantics.

It's a long philosophical story,
but one whose development is worth noting if the impression is still current
among mathematicians and logicians that intuitionists somehow don't make
contact with the real world, or don't take it sufficiently into account. On the
contrary, the Dummettian can claim that once one *does* take the physical
reality of actual communication into account, one is led along a justificatory
path to intuitionism.

May I recommend, Steve, that you take a look at my book The Taming of The True,
Oxford University Press, 1997?  The argument is developed much more fully there.

Neil Tennant