FOM: Visual proofs -- two examples

[Joe Shipman]

Moshe' Machover wrote:

> By a harmless extension of terminology, an outline from which it is clear
> how a proof in the strict sense can be constructed is also called a "proof".
>
> Occasionally, an intuitive explanation why a proposition is true is such
> that it can be easily converted into a proof. In such cases the intuitive
> explanation can itself be called a "proof"--again by a harmless extension
> or abuse of terminology. Examples of such `visual proofs' were given by
> Shipman. But often an explanation, no matter how *intuitively* persuasive,
> cannot be so easily converted into a proof.

You're assuming something I'm not ready to assume yet.  The reason I presented
those two proofs was because I wanted FOMers to elucidate

1) what it was about THOSE proofs that made them convincing
2) why we are persuaded that the proofs could be "easily converted" into a
rigorous sentential proof.

It is not obvious to me that 1) and 2) are the same.  Can you give an example
of a proof that is as "intuitively persuasive" as the two I gave that cannot be
easily converted into a proof?

There is a pragmatic assumption experienced mathematicians make, that a proof
which is sufficiently convincing can be converted to a rigorous sentential
proof.  This assumption is justified by experience.  It is similar to the
common assumption (Church's thesis) that any function we can calculate by an
effective procedure is recursive.  Many of us accept Church's thesis without
ever having gone through the technical work of constructing a universal Turing
machine, showing the equivalence of many independent definitions of
computability, following Turing's introspective justification of his model,
carefully verifying the existence of an algorithm in some real examples, and so
on; those of us who have done that work have more confidence in Church's
thesis.

Similarly, we accept the thesis that an argument which meets the ordinary
professional standards for publishable proof can be converted to a rigorous
sentential proof, and those of us who have carefully studied Frege, Hilbert,
and Godel and done some serious technical study in Set Theory have more
confidence in this thesis.  HOWEVER, the variety of types of reasoning in
published proofs is MUCH greater than the variety of effective procedures in
published algorithms, so that many of us do NOT have firsthand experience
trying to convert certain types of reasoning into a rigorous formalized proof.
The two "visual proofs" I presented are good examples because for many people
it's only obvious the proofs are "convertible" because the thesis is accepted;
for others who have worked with these types of proofs extensively it is clear
the proofs are "convertible" in a stronger sense (and only for this second
group could it be said that the proofs were *easily* convertible).

I would like people to explain why these proofs, which are only persuasive
because of the pictures they evoke, are rigorizable without begging the
question by assuming that anything that is persuasive is rigorizable.  An
analysis of the role of the pictures is probably a necessary part of such an
explanation.  I want to be able to call the arguments I presented "real proofs"
and not just intuitive arguments that happen to be rigorizable but could just
as easily not have been.  I can do this if there is a general explanation of
"visual proofs" which makes it clear that all the techniques used in my
arguments were fully rigorizable; this could also help us find examples of
visual arguments that are *not* fully rigorizable.