[FOM] Formalization Thesis
joeshipman at aol.com
Mon Jan 28 01:09:23 EST 2008
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
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".
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
>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
attitude towards geometric proofs of geometric results that not
seems to be able to "see"? Jaffe and Quinn touched on this subject in
their famous article on "Theoretical Mathematics":
An important part of the culture of mathematics is that a proof should,
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
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
way. My current instinct is to say that when Thurston gives a
proof of a geometric result which others can't quite follow, it's
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*
the visually impaired to check the proof. Would you be willing to go
far as this, when you argue that geometry defies discretization?
Something similar happens in set theory; if someone claims to be able
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
formulated as specific, discrete *axioms*. The conceptually impaired
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.
FOM mailing list
FOM at cs.nyu.edu
More new features than ever. Check out the new AOL Mail ! -
More information about the FOM