[FOM] Formalization Thesis

[Timothy Y. Chow]

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