Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!iuvax!cogsci!dave
From: dave@cogsci.indiana.edu (David Chalmers)
Newsgroups: comp.ai
Subject: Re: Natural Paradox
Keywords: Counterexample, Evidence, Belief, Proof, Provability
Message-ID: <17482@iuvax.cs.indiana.edu>
Date: 11 Feb 89 05:55:27 GMT
References: <1706@tank.uchicago.edu> <9526@ihlpb.ATT.COM> <44585@linus.UUCP> <9@UNIX386.Convergent.COM>
Sender: root@iuvax.cs.indiana.edu
Reply-To: dave@duckie.cogsci.indiana.edu (David Chalmers)
Organization: Concepts and Cognition, Indiana University
Lines: 41

In article <9@UNIX386.Convergent.COM> mark@UNIX386.Convergent.COM (Mark Nudelman) writes:
>A "proof" is a sequence of symbolic
>manipulations which starts with a set of axioms and ends with the 
>statement to be proven, following a certain set of rules for the
>manipulations along the way.  If a statement is "provable", it means
>such a sequence exists; this sequence is the "proof" for the statement.
>But what does it mean to prove that a statement is provable?  If a 
>statement is provable, then by definition a proof exists; exhibiting 
>this proof would seem to prove that the statement is provable.  Whether 
>or not any human being at any particular time in history is actually 
>aware of the proof is irrelevant; if the proof exists, then the statement 
>is provable; and exhibition of the proof is proof that it is provable.
>For a statement to be "provable, but not provably provable" would seem to
>mean that a proof exists, but cannot be exhibited.
 
Thanks Mark.  You're absolutely right.  Funnily enough, this is exactly
what I said 2 weeks ago in the posting which brought up the discussion
of provability.  As I said back then: if a statement is provable, it is
provable that it's provable.  All this discussion of Fermat's Last
Theorem (and Rolle's Theorem, I ask you!) is missing the point
completely.

As you say: it is part of the very essence of a proof that it be a 
sequence of symbols.  And obviously any sequence of symbols can be
exhibited.  (And just in case anyone gets any funny ideas: no, it
couldn't be the case that we couldn't PROVE that this sequence of
symbols was a proof - this is built into the defintion.)  So given any
proof, all we have to do is exhibit it and we've proven that we have a
proof.  (If you want to be totally rigorous, you can accompany the
exhibition with a detailed demonstration that logical rules are being
obeyed.)

The only way the general principle of "provability implies provable
provability" could fail to hold, is as you say if we had some system
where a proof could 'exist' but be unable to be written down.  Now
this seems totally contradictory to the idea of 'proof' to me - but
perhaps some people might be willing to entertain the idea.  All I can
say is that it wouldn't happen in normal mathematics.  It would have to
be in one of those "weird logics" that I mentioned in my first posting.

    Dave Chalmers