FOM: Re: Proofs

[Pat Hayes]

[An earlier response to Joe Shipman (to which he has already replied).
Submitted for information and archival purposes.]

>>[Hayes]
>>I suspect that you and I mean different things by "proof". It sounds like
>> that for you, a proof is something that suffices to convince the reader
>> that a proposition is true. That isnt what I mean by 'proof': for me, a
>> proof is a *rigorous demonstration* that a proposition *must be* true,
>> ultimately including all the details needed to ensure the rigor. Thus, your
>> notion of proof is ultimately a psychological notion, whereas for me it
>> most emphatically cannot rely on psychology.
>
>[Shipman]
>You are drawing a sharp line where none exists.  I am sure you do not mean a
>completely formalized proof with EVERY step filled in, because those are
>incredibly tedious.

No, that is exactly what I mean. A proof, strictly speaking, should be
completely formalised and mechanically checkable. I believe this is
essentially the accepted standard of a completely rigorous proof throughout
most of mathematics, in fact. While many published proofs, being intended
for reading by human beings, dont meet that impractical standard, if there
is any point of doubt or debate in a proof, it is expected that the authors
of it could, in principle, provide all the relevant details. It will never
be acceptable in mathematics to just say that some conclusion is 'obvious',
if challenged to account for the reason for it.

  Any proof you accept will leave out details, but there will
>be enough there that you can fill in the gaps yourself.  My proofs were
>rigorous
>in the following sense: someone experienced in the fields of geometry (1st
>proof) or topology (2nd proof) would, after reading the proof reasonably
>closely, be convinced, not only that the theorems were true, but that all the
>details he wanted could be easily filled in on demand.  Someone like yourself,
>less experienced in those fields, might not see how to fill all the gaps and
>could properly ask for more detail.  This means that the notion of
>adequacy of a
>proof is relative rather than absolute (unless you get all the way down to a
>formalized proof in the predicate calculus from the ZFC set-theoretical
>axioms,
>suitable for machine verification, which I am sure you do not do).

Ahem. See above. That is exactly where one gets absolute, yes. Strictly
speaking - and now we are in the heady realms of philosophy of mathematics
- I would say that there isnt any 'real' absolute foundation, and that this
follows from the indeterminacy and incompleteness theorems, ie ultimately
from the liar paradox. So even the choice of ZFC is ultimately a social
choice, in a sense: but it is a social choice of what to use as a
foundation, not a completely free social relativity about what constitutes
a proof.

  Put another
>way, there are some proofs *you* will accept that some other people will not,
>insisting on more detail -- that does not mean that either you or they are
>wrong
>about the adequacy of the proof.

It seems to me that any precise notion of "proof" must be independent of
the psychological talents or education of the person reading it. If not,
there is no clear distinction between mathematics and any other area of
human discourse. People convince one another of the truth of propositions
in all manner of ways, but most of them arent called mathematical proofs,
and for a very good reason: they cannot be rendered into a sufficiently
exact and detailed form. Its the existence of this mechanically verifiable,
ultimately exact and rigorous mode of expression which makes mathematics
distinct from, say, moral philosophy or jurispudence. Even though
mathematicians (who are human, after all) often use informal ways to
communicate with each other, and rely on one another's insight and training
to understand what they say to each other, nevertheless without this
ultimate possibility of reduction to a rigorous demonstration of validity,
the claim to be doing mathematics seems to me to be quite arbitrary.

>> Issues of pedagogy and ease of comprehension are quite irrelevant to the
>> nature of proofs, in my sense (though they may well be important matters,
>> of course.) It is entirely possible that a proof might exist which cannot
>> be understood by a human being, perhaps because it is too long or too
>> intricate. Several recent famous proofs almost qualify here, notably the
>> Fermat conjecture and the 4-color theorem.
>
>I'm afraid that if you are not willing to insist that proofs be totally
>formalized this will always be an issue.  There will always be readers of
>greater and lesser degrees of sophistication, some of whom need more details
>filled in than others.
>
>> Heres an observation to justify my position. To a sufficiently
>> sophisticated reader, some theorems might just be *obvious* on inspection.
>> On your view, then, it seems, these wouldnt need any other proof: is that
>> right?
>
>This is an interesting question.  Consider the theorem "All but finitely many
>prime numbers are odd".  This is obvious on inspection, but it is still
>possible
>to logically reduce the theorem to even more obvious principles, so a "proof"
>still serves some purpose.  But if you only care about the theorem itself and
>not what it depends on, then there is no need for a proof.

How then do you know that it is true? It seems to me that this isn't
obvious *on inspection*, but only when recast into the form: "The only even
prime is the number 2"; and if ones attention were momentarily distracted
by other thoughts, even this might require a gentle reminder that an "even
prime" must be divisible by 1, 2 and nothing else, by definition. And now
you have a proof.

>> >Did you find that it failed to persuade you that the theorem
>> >was true?
>>
>> First, that's irrelevant to the question (see above); but in any case, yes,
>> it did fail: that is, I saw it as a kind of sketch narrative *about* how to
>> prove the theorem; it has the same kind of relationship to a real proof (in
>> my sense) as an artists sketch of a new building has to an architectural
>> builders plan. Given a certain degree of mathematical competence on the
>> part of the reader - enough to be able to fill in the details to get from
>> the sketch to the actual proof - then sketch might suffice to specify the
>> proof, but it does not by itself *constitute* a proof.
>
>So precisely what level of detail would make this a proof?  You seem to feel
>that there is some level of detail which is "enough" in an absolute sense,
>and I
>don't see how you can draw a line short of getting to something mechanically
>verifiable.

Thats where I draw the line, indeed.

 A fair criticism would be that there is a gap in the proof that a
>mathematician experienced in the field could not *immediately* fill; this
>is one
>standard for publishability, and if I had been able to post the diagrams with
>the proofs my proofs would certainly meet it.

My problem with this kind of criterion is that history is replete with
examples of incorrect but widely accepted 'proofs' which had gaps which
nobody knew about at the time. A century ago nobody had a proper
comprehension of infinity, for example. So are we to say that mathematical
truth changes when people understand new things?

[...]

>Would you like to claim that the articles in
>the Transactions of the American Mathematical Society are not real proofs
>because each one can only be understood by a mathematician trained in the
>relevant area of mathematics?

Well, such a claim would smack of hubris. But I think that if pressed, I
would indeed say this: but I would quickly add, that I am sure that both
the authors and the intended readers of such proofs have the skill and
competence to be able to fill in the missing details if the need were to
arise, and that if there were any gaps in the proofs so filled in, then
they could be found and perhaps corrected. There are many examples of such
gaps being found in published proofs after publication, and I note that
then they are no longer considered to have been valid proofs, even though
they were found convincing by all readers until that time.

.....>
>> I could 'draw' all the pictures, but your second proof left me unconvinced.
>> Most of it has nothing to do with pictures, but with things like infinite
>> combinatorics, continuity and localness, none of which play any pictorial
>> role in your argument as given.
>
>Yes, but at least one part of the proof (the commutativity of the
>connected sum
>operation) is essentially pictorial in the sense that it can be made rigorous
>and picture-free only at the cost of clarity.

Well, lets look at that. As I recall, the argument was that one could make
one of the knots much smaller than the other and then slide it along the
string through the second one. That sounds to me like an argument in what
might be called naive topology (on the model of 'naive physics'), ie a kind
of common-sense grasp of what could be done in a world where things like
strings and knots were arbitrarily elastic or arbitrarily thin. Now,
formalising this kind of reasoning is an active area in AI, but it doesnt
seem to me to have anything *pictorial* about it. For example, it is
impossible to draw a picture of an arbitrary knot, yet this argument about
sliding a small one through a big one obviously works for any two knots.
The only thing that is 'pictorial' is really a piece of spatial reasoning:
that if a knot is expanded enough then the string can be surrounded by an
arbitrarily thick 'tube' of free space, and contrariwise that any knot can
be shrunk to fit entirely within a ball of a given radius. Passing that
ball along the tube is what gives the argument you need. But again, this
isnt a diagram, or even a movie, since it obviously works for *all* knots.

...
>As always, the diagrams help make one's UNDERSTANDING of the proof so
>clear that
>it is easy to fill in all the details; I admit this is an informal process and
>the diagrams play no formal role, but the point is that somehow they
>ensure that
>the filling in of the formal details will be easy and straightforward.

OK, again I suspect we are at cross purposes. Given my background in AI, I
can't accept psychological goings-on as just 'given'. If an ability to see
is considered part of a proof, then the processes of visual comprenesion
involved are part of the full proof, and they need to be made explicit.
Maybe the resulting proof will be ultimately checkable only by a machine
with an eye, but it still needs to be all  made explicit somehow to qualify
as a true proof.

Best wishes

Pat Hayes

---------------------------------------------------------------------
IHMC, University of West Florida		(850)434 8903   home
11000 University Parkway			(850)474 2091   office
Pensacola,  FL 32514			(850)474 3023   fax
phayes at ai.uwf.edu
http://www.coginst.uwf.edu/~phayes