FOM: Reply to Hayes on proofs

Kanovei kanovei at wminf2.math.uni-wuppertal.de
Wed Mar 3 03:30:07 EST 1999


> From: Joe Shipman <shipman at savera.com>
> Date: Tue, 02 Mar 1999 13:03:43 -0500

(Citing, probably, 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. 

As a matter of fact, any existing proof (with very 
few exceptions made just for purpose of demonstration 
of some human or computer's skills) 
is a text (that may include diagrams) 
which convinces (or sometimes does not 
convince) the reader that a proposition is true. 

The only alternative is a proof in formal sense, that 
is, a sequence of symbols which satisfies known rules 
and this fact can be checked by a computer. 

The only real use of this kind of proofs 
(let alone computer "provers" and where they are useful) 
is that the very existence of them 
(I mean: the belief that any correct proof can be 
transformed into a formal proof, which someone 
called the Zermelo thesis) 
shows that the mathematical truth is independent 
of views and attitudes of particular members of 
the mathematical community.  

V.Kanovei



More information about the FOM mailing list