FOM: intuitionistic mathematics and building bridges

[Vaughan Pratt]

From: Stephen Simpson
>Second, we need to remember that the double negation transform is
>purely formal does not respect philosophical motivation.

I beg to contradict.  Double negation as a transformation is much more
than formalism.  Look at the meanings of intuitionistic formulas, which
form a Heyting algebra.  Double negation translates those meanings upwards
to the nearest element of the Boolean algebra canonically embedded in
that Heyting algebra.

A philosophically well motivated interpretation of this motion is that it
carries the truth value of the proposition "A" to that of the proposition
"surely A", where "surely" satisfies

	surely surely = surely
	A -> surely A             (but not conversely) 
	surely not = not surely   (so this is a strong form of surely)
	etc.

To see the philosophical motivation here, think what "not not A" says:
it says that the absurdity of A is absurd.  While this is not quite
as strong as flatly asserting A, it is nevertheless a strong vote of
confidence in A that can be succinctly put as "surely A".

It has been my impression from having dealt with a lot of lawyers over
the last twenty years that the logic of the legal profession is rarely
Boolean, with a few isolated exceptions such as jury verdicts which permit
only guilty or not guilty, no middle verdict allowed.  Often legal logic
is not even intuitionistic, with conjunction failing commutativity and
sometimes even idempotence.  But that aside, excluded middle and double
negation are the exception rather than the rule.

Lawyers aren't alone in this.  The permitted rules of reasoning that
go along with whichever scientific method is currently in vogue seem to
have the same non-Boolean character in general.

The very *thought* of a lawyer or scientist appealing to Peirce's
law, ((P->Q)->P)->P, to prove a point boggles the mind.  And imagine
them trying to defend their use of that law by actually proving it:
the audience would simply ssume this was one of those bits of logical
sleight-of-hand where the wool is pulled over one's eyes by some sophistry
that goes against common sense.

If you treat intuitionism as pure formalism and pretend it is meaningless
then you are at risk of committing the same fallacy as David Hilbert and
Roger Penrose (to pick just two prominent offenders), namely that not
having double negation and excluded middle as laws ties one's hands.
Goedel realized early on the fallacy of this reasoning when he showed
one way of embedding classical arithmetic in intuitionistic.

Goedel's translation can be understood as pure formalism, but this
gives less insight than when you understand it in terms of meaning,
namely as a meaning-preserving translation.  What it demonstrates is that
intuitionistic arithmetic, far from being a feeble fragment of classical
arithmetic, can be interpreted as a rich tapestry that double negation
collapses to a coarse canvas.  (Well, I exaggerate a little for effect,
maybe the gap isn't quite that large, but the gap does exist, at least
to the extent that it is widely presumed not be closable naturally.)

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

It is only that way when one ignores enough nuances to fit the world
to Boolean logic.  Boolean logic is a Procrustean bed of a particularly
constraining kind.

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

What are you assuming here?  That mathematical constructions are mental
while mathematical objects are real?  Come on now.  In the mathematical
universe both are equally real (in the same sense that the construction
of a building is as real as the building itself, and waves are as real as
particles), while in the real world both spring from the mathematician's
fevered brow.

Constructivism in mathematics is no more or less mental than objectivism
in mathematics, and no more or less applicable to the real world.
The only things Boolean about the real world are its Boolean models.

Vaughan Pratt