[FOM] Formalization Thesis

[joeshipman@aol.com]

This was discussed a few years ago here. My take is that the 
mathematicians who understand these visual proofs have always been able 
to fill in enough details when pressed, that those who can't "see" 
things the same way will still accept the proof.

However, this is an empirical observation, and I have no a priori 
reason to believe it should always be true; and it may require a great 
deal of work by both prover and verifier, so there ought to be 
borderline cases where it has not yet been done to everyone's 
satisfaction.

In other words, something essential is lost in taking out the "visual" 
elements of the proof; but the result of this formalization, though 
unsatisfactory by some criteria, still preserves enough meaning that 
the theorem in question is not doubted.  (It would be remarkably 
interesting to have a counterexample, which would represent a type of 
impasse that, while not unprecedented in the history of mathematics, 
has not been seen for many decades.)

Another way in which mathematics may fail to be fully formalizable 
today involves the work of mathematical physicists like Witten, who 
often use physical intuition and principles of theoretical physics to 
argue that certain results in pure mathematics ought to be true -- 
their track record has been quite good, good enough to get Witten a 
Fields Medal, and I'm not sure that the failure to reduce much of this 
work to ZFC-theorems justifies dismissing it as "not mathematics".

-- JS

-----Original Message-----
From: Timothy Y. Chow <tchow at alum.mit.edu>
To: fom at cs.nyu.edu
Sent: Sat, 26 Jan 2008 3:08 pm
Subject: Re: [FOM] Formalization Thesis



Arnon Avron wrote:
>However, it is very doubtful that all geometric concepts and methods 
of
>proofs can be faithfully expressed in discrete languages.

I can see the intuition behind your doubts, and there is some force to
them.  Suppose we grant your hypothesis for a moment.  What then is 
your
attitude towards geometric proofs of geometric results that not 
everyone
seems to be able to "see"?  Jaffe and Quinn touched on this subject in
their famous article on "Theoretical Mathematics":

http://arxiv.org/abs/math/9307227

An important part of the culture of mathematics is that a proof should, 
in
principle, be checkable by anyone who is willing to put in the effort.
The fact that certain proofs, such as that of the four-color theorem or 
of
the classification of finite simple groups, threaten to violate this
principle is what lies behind the complaints that one sometimes hears
voiced about them.

The notion that some geometric proofs may be *fundamentally*
"undiscretizable" threatens to violate the same principle in a 
different
way.  My current instinct is to say that when Thurston gives a 
geometric
proof of a geometric result which others can't quite follow, it's 
because
he has left out details, and if he gave those details then anyone else
could check the proof.  But there's an alternative view, which is that
there *aren't* any missing details; some proofs may be visualizable by
some people but not by others, and there may not be *any way at all* 
for
the visually impaired to check the proof.  Would you be willing to go 
as
far as this, when you argue that geometry defies discretization?

Something similar happens in set theory; if someone claims to be able 
to
visualize inaccessible cardinals then he can "prove" that ZFC is
consistent, and someone who lacks that ability cannot check the proof.
But in the set-theoretical case, the statements in question can be
discretized, and the offending "unvisualizable" statements can be 
clearly
formulated as specific, discrete *axioms*.  The conceptually impaired 
can
verify everything except the *truth* of said axioms, and hence the
"damage" is contained and limited.

But if methods of geometrical proof cannot be discretized, then I don't
see how the damage can be limited in such a clean manner.

Tim
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom


________________________________________________________________________
More new features than ever.  Check out the new AOL Mail ! - 
http://webmail.aol.com