FOM: Visual proofs -- two examples

[Moshe' Machover]

At 10:12 am -0500 1/3/99, Joe Shipman wrote:

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

I can only speak for myself. I found these proofs not only visually
persuasive; but examining them step-by-step I could see how to turn them
into logically correct proofs.

>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?

Clearly, if you can see how to turn a visual/intuitive argument into a
proper proof, then it is persuasive, but the converse is false.

There are many examples of arguments that seem visually persuasive but
cannot be turned into a proper proof *except by adding an axiom or
condition, or modifying one of the key definitions, or proving a lemma that
turns out to be quite hard to prove*.

Here are a few such examples (none of them terribly original...):

(i) Euclid's proof that an equilateral triangle can be constructed with a
given side (additional postulate needed for correct proof);

(ii) Euler's formula for the vertices, edges and faces of polyhedron
(famous case-study by Lakatos; definition of polyhedron had to be worked
out).

(iii) Any visual argument that takes for granted Jordan's curve theorem
(hard `lemma' needed; think of such an argument presented *before* Jordan
had proved his theorem!)

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

I think it is the other way around: they regard a purported proof as
convincing, hence a real proof, if they can see how to convert it into a
correct sentential proof (of course, I don't mean a *formalized* proof; it
takes an experienced logician to see how to formalize a correct informal
proof).

>It is similar to the
>common assumption (Church's thesis) that any function we can calculate by an
>effective procedure is recursive.

I don't think this is the correct analogue. Rather, the correct analogue is
an argument `by Church's Thesis' that a *particular* function defined in
intuitive verbal terms is recursive. (This kind of argument is often used
by Rogers in his book.) I would accept such an argument as convincing only
if I can see how the appeal to Church's Thesis can be eliminated (say by
using the Recursion Theorem etc.).

[...]

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

Personally, I don't think that proofs, which are *only* persuasive because
of the pictures they evoke are always rigorizable--except by adding an
axiom or a condition, or modifying a key definition or by a similar device.
But then what is ultimately proved is not the same proposition as the one
that the original `proof' purported to prove.



  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %%  Moshe' Machover                 | E-MAIL: moshe.machover at kcl.ac.uk %%
  %%  Department of Philosophy        | FAX (office)*: +44 171 873 2270  %%
  %%  King's College, London          | PHONE (home)*: +44 181 969 5356  %%
  %%  Strand                          |                                  %%
  %%  London WC2R 2LS                 |  * If calling from UK, replace   %%
  %%  England                         |    +44 by 0                      %%
  %%  http://www.kcl.ac.uk/kis/schools/hums/philosophy/staff/moshem.html %%
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%