FOM: Visual proofs -- two examples (Reply to Machover)

[Joe Shipman]

Moshe' Machover wrote:

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

So could I, because I have studied enough of these proofs in my day -- but a
freshman calculus student who knows nothing of the degree of rigor we are talking
about would still find the first proof and the lemma (commutativity of connected
sum) used in the second proof completely convincing FOR THE RIGHT REASONS.  (Note
that I did not cite the second proof as a whole, since there is a tricky little
compactness argument at the end.)  Furthermore, the way I would "rigorize" those
proofs would be extremely cumbersome compared to the original "intuitive" proof, so
cumbersome that I would feel something essential was being lost.

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

But did you find my "intuitive arguments" *more* convincing because you also saw
how to turn them into a "proper proof"?  Could there possibly be an "intuitive
argument" that you found as convincing as my proofs that you could *not* also see
how to turn into a fully rigorous proof?

For both of us, there is probably an extremely strong correlation between finding a
mathematical argument convincing and seeing how it could be turned into a proper
proof; but that is only because we are well-trained in logic, set theory, and proof
theory.  For many mathematicians this is not the case; more interestingly, there
may be proofs in some areas of mathematics which specialists in the field find
convincing and publishable even though neither they nor we see how to formalize
them to the exacting degree logicians demand.  I would be surprised but not shocked
to learn of such proofs.

> 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!)
>

Three very good examples!  I'd mentioned Jordan's theorem earlier for precisely
this reason -- but as I remarked then, I do not know of any such
visually-obvious-but-unproven lemmas nowadays.  Does anyone have any candidates?
The Lakatos example is a little different, there was a real proof there that
remained valid, it was just unclear precisely how general a class of polyhedra the
argument applied to until the definitions were precisely nailed down.  Many
Euclidean proofs assumed continuity and betweenness postulates implicitly, but this
was not exactly a serious gap because as soon as the holes in the proofs were
noticed the implicit assumptions were immediately formalized [no one had any qualms
about simply *assuming* continuity and betweenness, which was not the case with the
Jordan Curve 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).

I don't agree; rendering those proofs into sentential form is the hard part, and
many would accept a visual argument as convincing *for the right reasons* before
they could convert it into sentential form (for example my argument for
commutativity of connected sum).

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

We're really saying the same thing here; an argument "by Church's thesis" that an
apparently effectively calculable function is recursive is like an argument "by
Zermelo's thesis" that an apparently proved theorem is derivable from the ZFC
axioms.  Logicians use this "argument" all the time.  Similarly, Church's thesis
itself is justified because every time we have tried to eliminate the appeal to it
by finding a real algorithm we have succeeded; I am pointing out that "Zermelo's
thesis" doesn't have quite the same level of justification because it seems much
more difficult to exhibit the desired ZFC-proof than the desired algorithm in the
earlier example.

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

That's why I used the word "these" in the above sentence.  But I'd like to see an
example of the type of proof you allude to, which is persuasive but not
rigorizable, that really is AS persuasive as the two proofs I showed.

-- JS