[FOM] Shapiro on natural and formal languages

[JoeShipman@aol.com]

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.)

http://www.cs.nyu.edu/pipermail/fom/1999-February/002665.html
http://www.cs.nyu.edu/pipermail/fom/1999-February/002677.html
http://www.cs.nyu.edu/pipermail/fom/1999-February/002715.html
http://www.cs.nyu.edu/pipermail/fom/1999-March/002725.html
http://www.cs.nyu.edu/pipermail/fom/1999-March/002728.html
http://www.cs.nyu.edu/pipermail/fom/1999-March/002731.html
http://www.cs.nyu.edu/pipermail/fom/1999-March/002734.html
http://www.cs.nyu.edu/pipermail/fom/1999-March/002751.html
http://www.cs.nyu.edu/pipermail/fom/1999-March/002755.html

-- Joe Shipman