FOM: Reply to Hayes on proofs

[Kanovei]

> 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