Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!ames!oliveb!pyramid!prls!philabs!linus!mbunix!bwk
From: bwk@mbunix.mitre.org (Barry W. Kort)
Newsgroups: comp.ai
Subject: Re: Natural Paradox
Summary: What about nonconstructive existence proofs?
Keywords: Counterexample, Evidence, Belief, Proof, Provability
Message-ID: <44698@linus.UUCP>
Date: 10 Feb 89 19:48:30 GMT
References: <1706@tank.uchicago.edu> <9526@ihlpb.ATT.COM> <44585@linus.UUCP> <9@UNIX386.Convergent.COM>
Sender: news@linus.UUCP
Reply-To: bwk@mbunix.mitre.org (Barry Kort)
Organization: Moribund Corporation, Seventh Chapter, DE
Lines: 11

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?

--Barry Kort