[FOM] Shapiro on natural and formal languages

[Vladimir Sazonov]

JoeShipman at aol.com wrote:

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

My comment:


Even if Arnon was referring not to classical Euclid-style proofs, my
point is that such kind of geometrical reasoning is also a kind of
language - a geometrical "natural" (informal) language. Pictures and
their fragments are like phrases having some coherent meaning. There
are various such non-verbal languages (say, the language of ballet,
etc.).

[By the way, I should tell I that did not read Shapiro' book, have
no personal opinion on it and rather comment on comments only.]

On the other hand, visual informal proofs are very good, but only
to "have a picture in the head" or to develop some idea. A highly
important step, but not the whole story. If such a "proof" is unclear
how to formalize (not necessary in the framework of FOL - any kind of
formalization might be appropriate) then this is only a preliminary
(may be even completely wrong!) idea of a mathematical proof. That
is why Euclid-style proofs (which are more plausible to be formalized)
are more appropriate here to discuss.

Should not a good mathematical proof be both intuitive and sufficiently
formal?  Which way can this be done - via diagrammatic proofs mentioned
by Peter Smith or via FOL - does not matter. I think that visualized
FOL in "Tarski's World" and "Hyperproof" software of Barwise and
Etchemendy mentioned by Allen Hazen (with a different accent) is
another good illustration of this point and also that a formalism, like
this software, is nothing else but a tool for mechanizing our thought
and strengthening our intuition. Therefore there is also nothing
against intuition, natural language, visual proofs, informal proofs,
heuristics, etc. in formalist point of view on Mathematics when
formulated appropriately. Just vice versa.


Vladimir Sazonov