[FOM] Shapiro on natural and formal languages
JoeShipman at aol.com
Fri Nov 26 14:38:26 EST 2004
I believe Avron, in speaking of "geometrical ways of reasoning", was referring not (as Sazonov seems to suppose) to classical Euclid-style proofs , which can be put into a formal language relatively straightforwardly, but to what I prefer to call "visual proofs", where it is possible in practice for a mathematician to follow the proof only if he "has a picture in his head".
This was discussed in detail here in February and March 1999. Rather than repeat what I said then, I link to my postings, which include the relevant parts of the postings of Moshe Machover, Charles Silver, Pat Hayes, and Reuben Hersh, who were also participating in the discussion.
(Short summary for those who don't want to go through all the links: In my opinion, many real, published mathematical arguments involve a form of reasoning ("visual reasoning") that can NOT be straightforwardly rendered in a formal language, and that such reasoning CAN be (NON-straightforwardly) rendered in a formal language is a highly nontrivial sociological and epistemological fact about mathematics, similar in nature to (but deeper than) Church's thesis that informally given effective procedures can always be rendered algorithmic in the sense of Turing machines.)
-- Joe Shipman
More information about the FOM