hin9@sphinx.uchicago.edu (The Reverend w. No Name) (10/05/87)
I've ever seen was is What is the Name of This Book?, by Raymond Smullyan.
'This Sentence is Unprovable in System S.'
If it's false, it is provable in system S, which is impossible unless
S is inconsistent. Therefore, it is true. Therefore, it is unprovable
in system S.
I imagine it would get more complicated if you used multivalued logic.
--
The Reverend with No Name "I don't have to practice what I preach
@ The Lord Julius Cabal because I'm not the kind of person I'm
...ihnp4!gargoyle!sphinx!hin9 preaching to." - J.R. "Bob" Dobbs.mps@duke.cs.duke.edu (Michael P. Smith) (10/05/87)
In article <2362@sphinx.uchicago.edu> hin9@sphinx.UUCP (The Reverend w. No Name) writes: > > 'This Sentence is Unprovable in System S.' > > If it's false, it is provable in system S, which is impossible unless >S is inconsistent. Therefore, it is true. Therefore, it is unprovable >in system S. One reason the proof is so short is that you don't show how the provability of the godelian sentence in S would entail that S is inconsistent.
radford@calgary.UUCP (Radford Neal) (10/06/87)
In article <2362@sphinx.uchicago.edu>, hin9@sphinx.uchicago.edu (The Reverend w. No Name) writes: > [from] What is the Name of This Book?, by Raymond Smullyan. > > 'This Sentence is Unprovable in System S.' > > If it's false, it is provable in system S, which is impossible unless > S is inconsistent. Therefore, it is true. Therefore, it is unprovable > in system S. This is the standard approach, as taken by Godel. I've always found it a bit on the tricky side, though, and therefore harder to figure out than the following approach (which must have been discovered by people other than me too, though I don't know any references): 1) Insert standard proof that no algorithm can determine whether a given algorithm terminates in all cases. (HALTING PROBLEM) 2) Formal systems of logic, mathematics, etc. all come with an algorithm for determining whether a proof is valid. There is always a countably infinite number of proofs. 3) For any formal system there is an algorithm that will terminate with "yes" if a given statement is a theorem. It just needs to check each possible proof in turn. 4) Any interestingly comprehensive formal system of logic is capable of expressing such statements as "Algorithm X does not terminate". 5) No interesting formal system is both correct and complete. If it were, you could solve the halting problem by just searching for proofs of "Algoritm X terminates" and "Algorithm X does not terminate" and announcing the result when you find one or the other. This proof makes it much clearer than the standard one that the "problem" applies to any system that could be considered "formal". It also avoids the tricky self-reference stuff, though there's a bit of that in the proof of the halting problem itself. Radford Neal The University of Calgary
ma261aai@sdcc3.ucsd.EDU (Stephen Bloch) (10/09/87)
In article <10368@duke.cs.duke.edu> mps@duke.UUCP (Michael P. Smith) writes: > >In article <2362@sphinx.uchicago.edu> hin9@sphinx.UUCP (The Reverend w. No Name) writes: >> >> 'This Sentence is Unprovable in System S.' >> >> If it's false, it is provable in system S, which is impossible unless >>S is inconsistent. Therefore, it is true. Therefore, it is unprovable >>in system S. > >One reason the proof is so short is that you don't show how the >provability of the godelian sentence in S would entail that S is >inconsistent. If you accept the semantic definition of inconsistency, i.e. "S is inconsistent if it has a theorem which on the intended interpretation is false," it's obvious. If, however, you want a purely proof- theoretic definition, i.e. "S is inconsistent if every wff in it is a theorem," there is indeed some nontrivial content yet to come. The other reason it's so short is because it contains the word "this". Does "This sentence" mean the sentence following the one in which "this" appears, or the sentence preceding the one in which "this" appears (for both of which possibilities there are plentiful examples), or the one the author is thinking about at the moment the reader reads the word "this", or the sentence the _reader_ was thinking about at the moment the _author_ first typed the word "this", or any number of other possible sentences that aren't the intended one (which, after all, is a VERY unusual way to interpret the word "this")? I think to avoid this (literally), the shortest possible example looks something like <If you replace all but the first occurrence of <snark> in <If you replace all but the first occurrence of <snark> in <snark> with <snark>, the result is unprovable in system S.> in <If you replace all but the first occurrence of <snark> in <snark> with <snark>, the result is unprovable in system S.>, the result is unprovable in system S.> Such a sentence does not rely on an intuition that we all know what "this" means, but only on the notions of string sequence and substitution, which can easily be defined purely formally. It doesn't assume that everyone reading it correctly understands that "this sentence" is a self-reference, but actually CONSTRUCTS the sentence it's talking about, which just happens to be identical to itself. Aside: It disturbs me somewhat that if I wrote the same sentence using quotation marks " and ' that are undistinguished between left and right, I couldn't possibly make it both unambiguous and character- for-character self-referential. Does this perhaps say something about the inherent logical superiority of nesting syntax?
franka@mmintl.UUCP (Frank Adams) (10/10/87)
In article <1094@vaxb.calgary.UUCP> radford@calgary.UUCP (Radford Neal) writes: >[Re: proof of undecidability by unsolvability of the halting problem] >It also avoids the tricky self-reference stuff, though there's a >bit of that in the proof of the halting problem itself. There is, in fact, every bit as much tricky self-reference in the proof of the unsolvability of the halting problem as there is in Goedel's incompleteness proof. These two proofs (undecidability of formal systems and unsolvability of the halting problem) are so similar that I have always considered them essentially the same, although I haven't ever tried to see exactly how parallel they are. -- Frank Adams ihnp4!philabs!pwa-b!mmintl!franka Ashton-Tate 52 Oakland Ave North E. Hartford, CT 06108
tmoody@sjuvax.UUCP (T. Moody) (10/11/87)
How about...
"Is not a theorem" is not a theorem.
?
--
Todd Moody * {allegra|astrovax|bpa|burdvax}!sjuvax!tmoody * SJU Phil. Dept.
"The wind is not moving. The flag is not moving. Mind is moving."