[FOM] Re: Mathematical Experiments

[Bill Taylor]

Don Fallis <fallis at email.arizona.edu>  raises a very serious point here.

->Bill Taylor's essay seems to me to be a good presentation of
->mathematicians' standard view about mathematical evidence. 

Thanks!  I appreciate your kind words.

->However, it is not clear that deductive proofs do provide any more
->"validation" than some of these "almost-proofs of large-primeness."

I understand the concern entirely.  A proof spread over a great many pages
in a journal, and involving earlier results in unexpected ways, may well
be a lot less *psychologically* convincing than a Fermat-found prime.

But again you are talking of *mistakes* here; and anyone can make mistakes.
We do our best, and should have, and DO have, many ways to try to prevent
and correct them; the whole idea of publishing being one grand mega-try.

But again, mistakes are *mistakes*, not math.  Their possible presence is
a very real academic and social concern, but NOT a philosophical one.
At least, not a math-philosophical one.

And note, scientists have similar problems, concerning their own chief
method of validation, physical experiment.  They also have to deal with
possible mistakes, of equipment, methodology, or lab-theory compatibility.


This whole thing turns on the word "proof", I think.  When I said math's
final arbiter of validation was PROOF, it is easy to misinterpret.

"Proof" has two meanings in our field.  It would be good to have two different 
words for them, or phrases, or maybe just spell one with a capital P.

Proof-1 is a strictly formal object - a series of strings in a language,
following certain well-known rules.  It is NOT on its own a practical
validation method, it could not be, for all but the most baby examples.
It would be outrageously long and formidably incomprehensible if so written.
It's chief use mathematically is its mere existence as a fall-back position;
and, especially, that being strictly formal it is a mathematical object in
itself, and can thus be treated mathematically.  Thus proof theory.

Proof-2 is a far more informal object. It is the published version of a proof-1,
containing many informal short-cuts such as diagrams and explanations in natural
language.  Of course, we expect and require that it can ("in principle") be
exapanded into a proof-1, at least in any suspicious part, though usually
such challenges and rebuttals are also less than strictly formal.  But again,
the existence of a putative proof-1 is invaluable as a referent for validation.

A proof-2 should really be called a "proof outline", except that this phrase
is reserved for even more informal summaries where it is admitted that not all
the gaps and glosses have necessarily been successfully dealt with.

With this distinction between the two usages of "proof", I hope the differences
between (say) Wiles' proof of FLT and the almost-proof of some large prime are
clear cut. The former is a proof-2 which has (we hope) an equivalent, expanded,
proof-1.  This proof-1 a validation of the truth of FLT (even though we never 
see it). We are perhaps not fully sure yet that this can be done - that maybe
the proof-2 of FLT has an undetected subtle error.  After all, it already DID,
once; maybe it could again.  Opinions may differ, but they will NOT differ
on the philosophical significance of any final (unseen) proof-1.

The latter case, the (pseudo)prime thing, is as near to a proof-1 as we are
likely to see in serious math.  Its layout (in the form of computer printout)
would be virtually a proof-1 as it stood.  And, as Don observes, it is
psychologically (and perhaps academically) more compelling as evidence
that a proof-1 of some sort exists.  At least it would be, if it were done
for as many cases as theory requires.  But, OC, it is nowhere *near* a proof-1
as it stands, done for just 3 or 4 or 10 bases, because it does NOT have the
validation of a formal proof that math requires.  So it may be commercially
sound for coding, but is philosophically as unsound a piece of evidence as
any other sort of incomplete number-crunching.


The difference between the two usages of the word "proof" is well-known to
all serious mathies, (though NOT to many popularisers), and regarded by them
as vital; whereas it is not so regarded by physicists and maybe even many
applied mathematicians.

It is not new with me - it is (at least) as old as Frege; but for some reason
it never seems to get highlighted in FOM books as much as it should.

------------------------------------------------------------------------------
     Bill Taylor                     W.Taylor at math.canterbury.ac.nz
------------------------------------------------------------------------------
          Logic - used by mathematicians but not talked about,
                    talked about by philosophers but not used.
------------------------------------------------------------------------------