[FOM] Formalization Thesis
Timothy Y. Chow
tchow at alum.mit.edu
Sat Jan 26 15:08:07 EST 2008
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":
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.
More information about the FOM