Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!ames!oliveb!pyramid!ctnews!UNIX386!mark
From: mark@UNIX386.Convergent.COM (Mark Nudelman)
Newsgroups: comp.ai
Subject: Re: Natural Paradox
Keywords: Counterexample, Evidence, Belief, Proof, Provability
Message-ID: <9@UNIX386.Convergent.COM>
Date: 9 Feb 89 19:10:41 GMT
References: <1706@tank.uchicago.edu> <9526@ihlpb.ATT.COM> <44585@linus.UUCP>
Organization: Convergent Technologies, San Jose, CA
Lines: 40

In article <44585@linus.UUCP>, bwk@mbunix.mitre.org (Barry W. Kort) writes:
> In article <9526@ihlpb.ATT.COM> arm@ihlpb.UUCP (55528-Macalalad,A.R.) writes:
> 
>  > It would be very interesting, though, to see a statement which
>  > was 'provable' yet not 'provable' that it's 'provable.'
> 
> Consider the statement:
> 
> 	Fermat's Last Theorem is provable.
> 
> Many mathematicians believe the above statement to be true.
> (Otherwise, they wouldn't continue searching for a proof of
> Fermat's Last Theorem.)  But as of this writing, there is no
> proof that Fermat's Last Theorem is provable.
> 
> Perhaps Fermat's Last Theorem is true but unprovable.
> 
> --Barry Kort

Godel proved that any sufficiently powerful proof system has statements 
which are neither provable nor disprovable within the system.  FLT may
be one of these statements.  But that's not what the question was.  The
question is "are there statements which are provable, but not provably
provable?"  Actually, I'm having a rather difficult time understanding
what is meant by this question.  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.

Mark Nudelman
{sun,decwrl,hplabs}!pyramid!ctnews!UNIX386!mark