FOM: Reply to Hayes on proofs
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.
More information about the FOM