[FOM] Re: Shapiro on natural and formal languages

[Vladimir Sazonov]

JoeShipman at aol.com wrote:
 > I am intrigued by your remark
 >
 > "We can try to formalize such proofs very close to how
they appeared visually, not necessary in FOL. Moreover,
we could have a metatheorem on a translation from this
formalization to FOL or ZFC. "
 >
 > Can you please provide more information on what a
formalization of those proofs "very close to how they
appeared visually" would be like?


My reply:

I thought we are discussing on a general phenomena of visual proofs,
and I wanted to say that for some *typical* classes of visual proofs
it is possible, in principle, to have some natural way of transforming
them into rigorous ones. For each concrete example, this is, of course,
the art - there is no general rule. But it is quite natural and usual
that the initial idea may be straightforwardly used (in that or other
way) as a kernel part of the corresponding formal proof. This seems
evident for the proofs you presented. (I hope you would agree.) And
this is a good evidence that these proofs are really formalizable so
that it is not so interesting even to bother about this. It is so
clear how to do ... just a routine. The resulting formal proof will
be boring, but will follow, anyway, the initial idea, and it is crucial
from mathematical point of view that such a formal proof can be really
done.

That is, it is not a picture itself which serves as a proof, but our
reflection on how this pictural proof could be potentially formalized,
even if we reflect on this only subconsciously. Even if there are such
mathematicians-phenomenons who (almost!) always ignore proofs and rather
serve as an Oracle, they are doing that in the context of the whole
mathematics which is based on rigorous proofs. Other mathematicians
will reflect instead of the Oracle and will do the rest of (absolutely)
necessary work. Most probably they will never present absolutely formal
proof, but they will definitely convince themselves and other
mathematicians that this is possible. Otherwise, this is not a proof
at all. Just an illusion of proof, may be even wrong (useless) illusion.



Joe Shipman:

Example Theorem 1: The connected sum operation on knots is commutative.

Description of visual proof: shrink the first knot down so small that it 
can be moved along the loop around and past the second knot, then blow 
it up again.

The actual "visual proof" might be an animation showing this operation. 
  And of course, in this case it is not VERY difficult to convert the 
visual proof into a fully formalized one.  But I maintain that the 
effort involved in such a formalization is disproportionate --
that a person who simply accepts the simple visual proof as valid based 
on her visual intuitions without bothering to go through all the details 
of formalization may still claim to KNOW THE THEOREM TO BE TRUE, and 
there is nonthing unmathematical or insufficiently rigorous about her 
attitude, she believes the connected-sum theorem FOR THE RIGHT REASONS.



My reply:

First, not TRUE, but PROVABLE, formalizable. We cannot refer here
to truth, for example, because we already know that there are some
seemingly true facts which can be disproved (say, recall, the 
Banach-Tarski paradox and the existence of continuous curves with
very strange properties). I repeat, the point of the above visual
proof is that it gives an idea how to prove the theorem formally.
This is THE RIGHT REASON! That the the effort is disproportionate
does not matter. We cannot avoid this step, at least as a potential
one. This is the reality of mathematics.



Timothy Y. Chow wrote:
 > Joe Shipman clarified what he was asking for; to test my understanding,
 > let me suggest two candidates:
 >
 > 1. Every finite graph can be embedded in R^3 without crossings.
 >
 > 2. The trefoil knot cannot be unknotted in R^3.
 >
 > Both of these are visually obvious, and it seems any kind of
 > formalization is likely to lose something in the translation.

These even do not look as proofs. These are theorems looking
also quite plausible without any indication how to prove them.


Do these
 > then qualify?
 >
 > Vladimir Sazonov questions whether any so-called visual proof is really
 > anything more than a heuristic starting point if it's not clear how to
 > formalize it.  What do you say about #2 above?  This strikes me as an
 > example of something that is as obviously true as any standard axiom,


The role of axioms is not to represent truth, but to be a base for
derivation of proofs. Not every statement, even seemingly "true"
is appropriate for this role.


 > yet which I wouldn't call "linguistic" (even if one admits visual
 > languages).


I feel that this is somewhat out of the context.


It's also not immediately clear how to formalize it, but
 > formalization seems to reduce the clarity and certainty rather than to
 > increase it.


The role of mathematical proof is not clarity or certainty that
the proved fact is true. If you need clarity, just take #2 as it is
and forget on any mathematics. You will have what you really want:
clear fact, but not a mathematics. I think that this is also the
demonstration that the goal of mathematics is not truth. Otherwise,
mathematicians would not be so "stupid" by proving "evident facts".
Then, like physicists, they would prefer truth to proofs.


Finally, it seems to me that the question "How do we know that our 
mathematical formalization of these Theorems are appropriate?" raised
in the posting of Harvey Friedman is very important. As I understand,
it should be related with the thesis that mathematics is not about
the truth. However, it is unclear to me how can definitions be
"not only appropriate, but correct". Say, what is the difference?
I would be very grateful to Harvey Friedman for clarification.


Vladimir Sazonov