Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!purdue!mentor.cc.purdue.edu!l.cc.purdue.edu!cik
From: cik@l.cc.purdue.edu (Herman Rubin)
Newsgroups: comp.ai
Subject: Re: Natural Paradox
Keywords: Counterexample, Evidence, Belief, Proof, Provability
Message-ID: <1129@l.cc.purdue.edu>
Date: 12 Feb 89 11:46:39 GMT
References: <1706@tank.uchicago.edu> <9526@ihlpb.ATT.COM> <44585@linus.UUCP> <44698@linus.UUCP>
Organization: Purdue University Statistics Department
Lines: 34

In article <44698@linus.UUCP>, bwk@mbunix.mitre.org (Barry W. Kort) writes:
> In article <9@UNIX386.Convergent.COM> mark@UNIX386.Convergent.COM
> (Mark Nudelman) writes:
> 
>  > For a statement to be "provable, but not provably provable"
>  > would seem to mean that a proof exists, but cannot be exhibited.
> 
> Are there not examples of nonconstructive existence proofs in
> mathematics?  Couldn't one prove that a derivation necessarily
> exists without exhibiting the derivation?

A nonconstructive proof is still a formal sequence of statements 
satisfying certain rules.  And there have been situations in which
the existence of an integer, or a finite set of integers, has been
proved without exhibiting it.  But a systematic search would 
eventually find it.  This is quite different from nonconstructive
proofs such as the existence of a non-measurable set from the axiom
of choice.  In this case, the set can not be exhibited if certain
properties of the real numbers are consistent.

It is possible that there is a proof that something is constructible 
without having an explicit construction.  One could interpret this as
meaning that a statement can be provably provable without a proof
being known.  But a statement cannot be provable without the existence
of a proof found by a systematic search.  This exhibition would 
show that it is provably provable, etc.

Now it is possible for a sequence of statements all to be provable,
but it is not the case that there is a proof that they are all provable.
If mathematics is consitent, that is an example.
-- 
Herman Rubin, Dept. of Statistics, Purdue Univ., West Lafayette IN47907
Phone: (317)494-6054
hrubin@l.cc.purdue.edu (Internet, bitnet, UUCP)