staff_bob@gsbacd.uchicago.edu (bob kohout) (02/03/89)
In article <3091@silver.bacs.indiana.edu>, chalmer@silver.bacs.indiana.edu (david chalmers) writes... >In article <44071@linus.UUCP> bwk@mbunix.mitre (Barry Kort) writes: >>Consider, if you will, the following pair of sentences: >> >> "The following sentence is provable." >> "The preceding sentence is unprovable." >> >>The paradox seems to have vanished. The first statement >>can be both True and Unprovable. The second sentence >>can be both True and Provable. (But please don't ask >>me to supply the proof. I didn't say they were provable >>by *me*!) >> >>The point is twofold: Not all True sentences are provable >>and not all unprovable sentences are False. Thus we need >>a third category: Undecidable. >> >>We can then resolve the paradox by chastising both sentences >>for overstating the case. They could have gotten along >>very nicely if they had scaled back their dogmatic assertions >>along the lines of the second, more harmonious pair. > >Sorry. It's kind of obvious that if a sentence is provable, then >it's PROVABLE that it's provable. Because if a proof exists, >a PROOF that the proof exists just consists in displaying the >original proof. Got that? (There may be weird logics in which >this is untrue - for instance where a proof could 'exist' but be >unable to be constructed - but this kind of thing isn't relevant >here.) > Mr.Kort said that not all TRUE sentences are provable. This is a well known theorem, arrived at by Kurt Godel (o mit umlaut) in the earlier part of this century. It has nothing to do with wierd logics; it applies equally to any system suffienciently powerful to embody basic arithmetic. Even your statement that 'if a sentence is provable, then it's PROVABLE that it's provable' does not hold. For many years, one could not show the four color problem was provable, and yet it was. Only upon discovery of a proof is your claim valid, but the 'provability' of a logicaL statement is invariant. Basically, Godel has shown that for any sufficiently powerful system of logic, either it is possible to construct true statements which cannot be proven inside the system, or the system is inconsistant (which, for those of you not familiar with mathematics, is much, much worse. One can prove anything one likes in an inconsistant system.) Thus, certain 'sentences' are undecidable. >Here are your two statements again: > 1: Sentence 2 is provable. > 2: Sentence 1 is unprovable. > >So: if Sentence 1 above is True, then (by reading what it says) >Sentence 2 is provable. But as we've just said, this entails >that the statement "Sentence 2 is provable" is itself provable. >But this statement is just Sentence 1! So now we see that >Sentence 1 is provable, CONTRADICTING Sentence 2. So, oops, >now Sentence 2 is FALSE, so it can't be provable. > I'm sorry, what do you mean 'this entails that the statement...' ?' I think what you want to say is that if 1 is true, then we can use it to prove 2 true. In so doing, we 'prove' 1 also. This however is no proof, since we have had to assume 1 in order to prove 1. It is quite possible for 1 to be true, but not provable, without creating a contradiction. If we make it an axiom (by assuming its truth) then we are in effect altering the logical system we started with. The system then becomes A) Sentence 1 is true 1) Sentence 2 is provable 2) Sentence 1 is unprovable (plus the other rules of logic, which are implicit in the notion of 'provable', and which can theorectically be made explicit.) This system is inconsistant, since we can prove 1 by A and disprove it by 2. Thus this new system is worthless. Without introducing A as an axiom, and thereby making it possible to prove anything, how is it possible to prove 1? I am not saying that there is not a paradox here, I just don't follow your reasoning. People like Russell devoted their lives to the elimination of paradox from logical systems, in the faith that paradox was anathema to logic. In the more general case, Godel has proven that it is always possible to create a statement which, basically, states 'this statement is false' and yet cannot be proven inside of the system. This is not a shortcoming of English, it is a fundamental property of logic. Such statements may or may not be true, but they are undecidable. Bob Kohout
dave@cogsci.indiana.edu (David Chalmers) (02/03/89)
Newsgroups: comp.ai Subject: Re: Natural Paradox Summary: Expires: References: <1706@tank.uchicago.edu> Sender: Reply-To: dave@cogsci.indiana.edu (David Chalmers) Followup-To: Distribution: Organization: Concepts and Cognition, Indiana University Keywords: In article <1706@tank.uchicago.edu> staff_bob@gsbacd.uchicago.edu (bob kohout) writes: >In article <3091@silver.bacs.indiana.edu>, chalmer@silver.bacs.indiana.edu (david chalmers) writes: >>In article <44071@linus.UUCP> bwk@mbunix.mitre (Barry Kort) writes: >>>Consider, if you will, the following pair of sentences: >>> >>> "The following sentence is provable." >>> "The preceding sentence is unprovable." >>> >>>The paradox seems to have vanished. The first statement >>>can be both True and Unprovable. The second sentence >>>can be both True and Provable. >> >>Sorry. It's kind of obvious that if a sentence is provable, then >>it's PROVABLE that it's provable. Because if a proof exists, >>a PROOF that the proof exists just consists in displaying the >>original proof. Got that? (There may be weird logics in which >>this is untrue - for instance where a proof could 'exist' but be >>unable to be constructed - but this kind of thing isn't relevant >>here.) >> >Mr.Kort said that not all TRUE sentences are provable. This is a well >known theorem, arrived at by Kurt Godel... I know. I never argued with this. I made the "provable implies provably provable" comment to aid the demonstration that the above two sentences CAN'T be true simultaneously. (Coming up.) > >Even your statement that 'if a sentence is provable, then it's >PROVABLE that it's provable' does not hold. For many years, >one could not show the four color problem was provable, and yet it >was. Only upon discovery of a proof is your claim valid, but the >'provability' of a logicaL statement is invariant. This is incoherent. The "provability" of a statement is not dependent upon the capacities of us limited human beings to find and construct such a proof. This applies even when the statement whose provability we are investigating is of the form "Statement X is provable." "Provability" is a well-defined mathematical notion that is independent of arbitrary human exigencies, in the same way that, say, "triangularity" is. Just as the four-color theorem was in fact TRUE even before 1974 (when some people found the proof), it was also provable before then. Upon Haken & Apell's proof in 1974, then humans DISCOVERED for sure that not only was the theorem true, but that it was provable, and that it was provable that it was provable, and so on. But none of these are time-dependent concepts. >>Here are your two statements again: > >> 1: Sentence 2 is provable. >> 2: Sentence 1 is unprovable. >> >>So: if Sentence 1 above is True, then (by reading what it says) >>Sentence 2 is provable. But as we've just said, this entails >>that the statement "Sentence 2 is provable" is itself provable. >>But this statement is just Sentence 1! So now we see that >>Sentence 1 is provable, CONTRADICTING Sentence 2. So, oops, >>now Sentence 2 is FALSE, so it can't be provable. >> > >I'm sorry, what do you mean 'this entails that the statement...' ?' >I think what you want to say is that if 1 is true, then we can >use it to prove 2 true. In so doing, we 'prove' 1 also. This >however is no proof, since we have had to assume 1 in order to >prove 1. It is quite possible for 1 to be true, but not provable, >without creating a contradiction. If we make it an axiom (by >assuming its truth) then we are in effect altering the logical >system we started with. You've missed the point, or maybe I wasn't clear enough. I was demonstrating that it's impossible for both statements to be true simultaneously. To do this, I ASSUMED that S.1 was true, and showed that under this assumption S.2 has to be false. (And along the way I showed that all kinds of other paradoxical things were entailed). Another way of looking at this is to realize that, by my previous argument, it is impossible for a statement of the form "X is provable" to be true but unprovable. So your (and BK's) statement, that it is possible for Sentence 1 to be true but unprovable, is wrong. > >I am not saying that there is not a paradox here, I just don't follow >your reasoning. People like Russell devoted their lives to the elimination >of paradox from logical systems, in the faith that paradox was anathema >to logic. In the more general case, Godel has proven that it is always possible >to create a statement which, basically, states 'this statement is false' >and yet cannot be proven inside of the system. This is not a shortcoming of >English, it is a fundamental property of logic. Such statements may or >may not be true, but they are undecidable. That's absolutely right. If we ever have a genuine paradox, grounded in a well-defined system of reality (or mathematical reality), then our system falls apart. Given that we don't want our system to fall apart, then like Russell we have to make damn sure that there aren't any real paradoxes. The usual way to do this is to deem statements like "This sentence is false" ill-defined or meaningless. Godel's great insight is that statements like this (well, actually like "This statement is unprovable") can actually be grounded (with a lot of work) in concrete mathematical reality (if that's not a contradiction in terms). After he did this, the "meaningless" escape route was no longer available, so people had to accept "true but unprovable" statements. Very annoying, but a small sacrifice to make to save all of mathematics from destruction. (See my last posting for more on Godel, paradoxes and meaninglessness.) Dave Chalmers
arm@ihlpb.ATT.COM (Macalalad) (02/03/89)
In article <1706@tank.uchicago.edu> staff_bob@gsbacd.uchicago.edu (bob kohout) writes: <to David Chalmers> > >Even your statement that 'if a sentence is provable, then it's >PROVABLE that it's provable' does not hold. For many years, >one could not show the four color problem was provable, and yet it >was. Only upon discovery of a proof is your claim valid, but the >'provability' of a logicaL statement is invariant. > Sorry to jump into this argument, but isn't the 'provability' of the 'provability' of a logical statement also invariant? This doesn't take away too much from the rest of your argument, which basically distinguished between 'true' and 'provable' statements. It would be very interesting, though, to see a statement which was 'provable' yet not 'provable' that it's 'provable.' -Alex
ap1i+@andrew.cmu.edu (Andrew C. Plotkin) (02/05/89)
/ It would be very interesting, though, to see a statement which / was 'provable' yet not 'provable' that it's 'provable.' How would you know it if you saw it? If you could point at it and say "That statement is provable, but you can't prove it!" how would you know that the first part of the claim is true, without invalidating the second part? --Z
bph@buengc.BU.EDU (Blair P. Houghton) (02/05/89)
In article <kXuo9-y00V4=88uEVm@andrew.cmu.edu> ap1i+@andrew.cmu.edu (Andrew C. Plotkin) writes: >/ It would be very interesting, though, to see a statement which >/ was 'provable' yet not 'provable' that it's 'provable.' > >How would you know it if you saw it? If you could point at it and say "That >statement is provable, but you can't prove it!" how would you know that the >first part of the claim is true, without invalidating the second part? Remember Rolle's theorem? --Blair "Rather, Rolle's conjecture..."
ap1i+@andrew.cmu.edu (Andrew C. Plotkin) (02/06/89)
/>/ It would be very interesting, though, to see a statement which />/ was 'provable' yet not 'provable' that it's 'provable.' /> />How would you know it if you saw it? If you could point at it and say "That />statement is provable, but you can't prove it!" how would you know that the />first part of the claim is true, without invalidating the second part? / /Remember Rolle's theorem? No. Clarify? --Z
bwk@mbunix.mitre.org (Barry W. Kort) (02/07/89)
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
dave@hotlr.ATT ( C D Druitt hotlk) (02/08/89)
In article <17167@iuvax.cs.indiana.edu> dave@duckie.cogsci.indiana.edu (David Chalmers) writes: > > This is incoherent. The "provability" of a statement is not dependent > upon the capacities of us limited human beings to find and construct > such a proof. This applies even when the statement whose provability > we are investigating is of the form "Statement X is provable." > "Provability" is a well-defined mathematical notion that is > independent of arbitrary human exigencies, in the same way that, > say, "triangularity" is. Just as the four-color theorem was in > fact TRUE even before 1974 (when some people found the proof), it was > also provable before then. Upon Haken & Apell's proof in 1974, then > humans DISCOVERED for sure that not only was the theorem true, but > that it was provable, and that it was provable that it was provable, > and so on. But none of these are time-dependent concepts. > > You've missed the point, or maybe I wasn't clear enough. I was > That's absolutely right. If we ever have a genuine paradox, grounded in a > well-defined system of reality (or mathematical reality), then our system > falls apart. Given that we don't want our system to fall apart, then like > Russell we have to make damn sure that there aren't any real paradoxes. The > usual way to do this is to deem statements like "This sentence is false" > ill-defined or meaningless. Godel's great insight is that statements like > this (well, actually like "This statement is unprovable") can actually be > grounded (with a lot of work) in concrete mathematical reality (if that's not > a contradiction in terms). After he did this, the "meaningless" escape route > was no longer available, so people had to accept "true but unprovable" > statements. Very annoying, but a small sacrifice to make to save all of > mathematics from destruction. (See my last posting for more on Godel, > paradoxes and meaninglessness.) > > Dave Chalmers > When I encounter something that doesn't make sense at first glance, I have two choices: File it away and keep listening or looking for further input to clarify (passive) or request further input. Seems to me that paradoxes and fuzzy sets are unavoidable. Why not admit this and focus more on procedures for handling them when they are encountered? Dave Druitt (the NODES) (201) 949-5898
goretsky@olivea.olivetti.com (David Goretsky) (02/09/89)
is examined in a book called "The Liar Paradox" (or something like that) which is either authored or co-authored by John Etchemendy (or was it John Perry?). I believe it's based on Barwise/Perry's Situation Semantics. it should put this whole silly thing to rest. go on. read it. and please explain it to me when you're done. thanks.
bph@buengc.BU.EDU (Blair P. Houghton) (02/09/89)
In article <0XvA3xy00Xoj82iV53@andrew.cmu.edu> ap1i+@andrew.cmu.edu (Andrew C. Plotkin) writes: >/>/ It would be very interesting, though, to see a statement which >/>/ was 'provable' yet not 'provable' that it's 'provable.' >/> >/>How would you know it if you saw it? If you could point at it and say "That >/>statement is provable, but you can't prove it!" how would you know that the >/>first part of the claim is true, without invalidating the second part? >/ >/Remember Rolle's theorem? > >No. Clarify? I don't know about how you learned Calculus, but when I went through it the first time the book mentions Rolle's theorem (having to do with the idea that a continuous function that is positive at one point and negative at another must be zero at some point in-between) and says it's gotta be true, but that they wouldn't dare prove it. Every other theorem in a first-year calc book gets proven. Rolle's doesn't. I've never seen a basic Calc book that proves it. That also means I've never seen it proven. I seem to remember someone along the lines of Einstein as having said that he couldn't prove it; but it's gotta be provable; it's the cornerstone of the proofs of almost every theorem that follows it in the book I first used. Okay, so they're provable, but can we prove that they're provable? It means we have to prove Rolle's Theorem. --Blair "Mathematically. Saying it's obviously true doesn't work in math. That's why it's math, and not theology."
bwk@mbunix.mitre.org (Barry W. Kort) (02/09/89)
In article <2073@buengc.BU.EDU> bph@buengc.bu.edu (Blair P. Houghton) writes about unproven theorems in calculus: > It means we have to prove Rolle's Theorem. I looked this up in Robert T. Seeley's book. Although the chain of lemma's, theorems, and proofs are lengthy, he does prove the Mean Value Theorem and Intermediate Value Theorem (including Rolle's Theorem) using the Maximum Value Theorem, which he proves in an appendix. (The Maximum Value Theorem states that a continuous function on a closed interval necessarily achieves a maximum (and a minimum) in the interval) I am not prepared to defend the rigor of Seeley's proofs, but his running commentary acnkowledged the difficulty of exhibiting the unbroken chain of proofs, which he evidently succeeds in doing. --Barry Kort
arm@ihlpb.ATT.COM (Macalalad) (02/10/89)
In article <2073@buengc.BU.EDU> bph@buengc.bu.edu (Blair P. Houghton) writes: > >I don't know about how you learned Calculus, but when I went through it >the first time the book mentions Rolle's theorem (having to do with the >idea that a continuous function that is positive at one point and >negative at another must be zero at some point in-between) More precisely, (or as precisely as I can be off the top of my head :-) given a function f that is continuous and differentiable on (a,b) such that f(a) = f(b) = 0, then there exists at least one c in (a,b) such that f'(c) = 0. >and says it's >gotta be true, but that they wouldn't dare prove it. Every other theorem >in a first-year calc book gets proven. Rolle's doesn't. I've never >seen a basic Calc book that proves it. That also means I've never seen >it proven. Come on, _every_ basic Calc book _I've_ seen proves it. The proof is very basic, and I could probably prove it right now, were I sufficiently motivated. I leave it as an exercise for the reader. (:-) >I seem to remember someone along the lines of Einstein as having said >that he couldn't prove it; but it's gotta be provable; it's the >cornerstone of the proofs of almost every theorem that follows it in >the book I first used. > >Okay, so they're provable, but can we prove that they're provable? Not to belabor the point, but the question of whether or not a theorem is provable or provable that it's provable, and so on, is entirely different from the question of whether _we_ can prove the theorem is provable, and the two should not be confused. To show that it is possible for a theorem to be provable yet not provable that it is provable, it is sufficient to show that there exists such a theorem, and it is not necessary to come up with a specific example. Of course, it is probably easy to show that a theorem which is provable is provable that it is provable, and were I sufficiently motivated.... (:-) The second question, which seems to me to be the more interesting question, involves how we come up with, or fail to come up with, proofs for theorems. This is a more psychological question, and one which is certainly appropriate for this group. Comments? -Alex
mark@UNIX386.Convergent.COM (Mark Nudelman) (02/10/89)
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
ap1i+@andrew.cmu.edu (Andrew C. Plotkin) (02/10/89)
/ > 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. In that case, the statement you made above is just false. We know lots of theorems that have been proved to be unprovable; F'sLT, so far, is not one of them. (A year ago or so, someone came up with a putative proof of the thing, which was being checked last I heard.) />How would you know it if you saw it? If you could point at it and say "That />statement is provable, but you can't prove it!" how would you know that the />first part of the claim is true, without invalidating the second part? / /Remember Rolle's theorem? /I don't know about how you learned Calculus, but when I went through it /the first time the book mentions Rolle's theorem (having to do with the /idea that a continuous function that is positive at one point and /negative at another must be zero at some point in-between) and says it's /gotta be true, but that they wouldn't dare prove it. Every other theorem /in a first-year calc book gets proven. Rolle's doesn't. I've never /seen a basic Calc book that proves it. Sitting here in the computer room, I asked a random person for a basic calc book; it had a proof of that theorem. (_Calculus_, James Stewart, Brooks/Cole Publishing). I vaguely recall having it proved in calculus. --Z
bwk@mbunix.mitre.org (Barry W. Kort) (02/11/89)
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
demers@beowulf.ucsd.edu (David E Demers) (02/11/89)
In article <44585@linus.UUCP> bwk@mbunix.mitre.org (Barry 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. We already know that {under appropriate circumstances} there are TRUE but UNPROVABLE statements; however, are there PROVABLE statements about which one cannot PROVE they are provable? I agree with the poster who argued no. If the statement is provable, then one simply needs to exhibit the proof in order to prove its provability. Dave DeMers demers@cs.ucsd.edu Computer Science & Engineering - C-014 UCSD La Jolla, CA 92093
dave@cogsci.indiana.edu (David Chalmers) (02/11/89)
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
bwk@mbunix.mitre.org (Barry W. Kort) (02/12/89)
In article <5898@sdcsvax.UUCP> demers@beowulf.UCSD.EDU (David E Demers) writes: > We already know that {under appropriate circumstances} there > are TRUE but UNPROVABLE statements; however, are there PROVABLE > statements about which one cannot PROVE they are provable? It depends on what you mean by "one" in the above sentence. Consider if you will the assertion, "The integer formed by 317 repetitions of the digit 1 is prime." I claim that the above assertion is true (but I don't know how to prove it). I also claim that the assertion is not only true, but provable. (But I don't know how to prove that claim, either.) > If the statement is provable, then one simply needs > to exhibit the proof in order to prove its provability. Evidently I have failed to supply the needed proof. So I clearly haven't proven that the assertion is provable. Nevertheless, I still claim it is the case that the assertion is both true and provavble. --Barry Kort
cik@l.cc.purdue.edu (Herman Rubin) (02/12/89)
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)