FOM: Visual Proofs: Reply to Silver and Hayes

[Joe Shipman]

Silver:
> What do you mean by a "rigorous sentential proof"?
Basically, a formal proof in the predicate calculus from some accepted
set of axioms -- these proofs (the objects of proof theory) are
"sentential" because they consist of sequences of sentences, each of
which is either an axiom or derivable from earlier sentences by a
logical rule.  I didn't simply want to say "formal" proof because some
of the discussion here has been about diagrammatic proofs that were
rigorous and formal but not sentential.

Hayes:
>Basically, your proofs aren't purely visual, and moreover they couldnt
be,
>in an important sense: they require an ability to generalise over
classes
>of pictures which cannot itself be represented pictorially.
I'm NOT claiming these proofs are "purely" visual, just that they have a
visual COMPONENT that is in some sense essential for understanding the
proof and translating it into a "rigorous" proof in a formal system.

>Similar objections apply throught the rest of your proof. You
constantly
>suggest 'pictorial' demonstrations which are intended to establish
>univerally quantified truths about all rectangles, all triangles, and
so
>forth; but you claim to demonstrate these by displaying single
pictures.
Wait a minute.  Are you now saying that my proof was not a "real
proof"?  Did you find that it failed to persuade you that the theorem
was true?  My point is that an appropriate picture often DOES suffice to
establish some statement in that it persuades people of the truth of the
statement (and probably also persuades them that a rigorous proof of the
statement can be obtained in a straightforward way).  In fact my proofs
didn't even draw pictures, just described pictures in words, but in such
a way that people who were able to imagine the pictures I was describing
would immediately assent to statements like "any triangle is equivalent
to a rectangle by finite decomposition" or "the connected sum operation
on knots is commutative".

>No; it shows (if anything) that *two* such squares can be 'merged'
while
>preserving areas. But your theorem requires this to hold for *any
finite
>number*: so your proof needs an inductive argument. Such "obvious"
>inductions are often not made explicit in informal reasoning, but they
are
>an essential part of a correct proof, as was painfully discovered by
>algebraists about 130 years ago.
I'm not claiming my proof didn't leave out any details, just that it is
sufficient to persuade some people of the truth of the theorem.  The
"inductive" part of the argument is of course implicit here and could
easily be made explicit; but in fact everyone here knows how to do that,
it is making the PICTORIAL part of the argument explicit enough that is
the interesting issue.

>... is actually a sophisticated piece of reasoning
>involving induction and a sound grasp of the notion of convergence. If
you
>were to try to make these proofs explicit, I think that the pictures
would
>turn out to be more like convenient annotations acting as memory aids
than
>part of the proofs themselves.
This doesn't follow -- you have shown that the pictures by themselves
are not sufficient, not that they are not necessary.  I agree that
pictures can serve as convenient memory aids, and if that is ALL they
are for these proofs it is still interesting to ask how they accomplish
that; but I don't think that is all that is going on.

-- Joe Shipman