Can Rosser 1936 be Extended? Alan Turing vs. Martin Davis et. al.
in [Logic]
|
Prev: Philosophy of mind is more important than the philosophy of language and epistemology
Next: Unsolvability of the Entscheidungsproblem as a Corollary of Gödel’s 2nd Theorem
From: Rupert on 31 May 2010 06:12 On May 30, 10:45 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > Everyone including Martin Davis (his anthology) says that Rosser 1936 > can't be extended because an inconsistent system proves everything and > so is complete (in a very bad way.) But Turing 1937 includes a > derivation of Rosser 1936. So what are the possibilities? > > 1. Turing 1937 is equivalent to Rosser 1936. > > 2. Martin Davis and everybody else are wrong. > > 3. They need to more closely examine the notion of extending a > theorem. > > 4. What? > > C-B Perhaps I will have a look at Turing 1937 and see what I think. But maybe you could tell us *exactly* what it is that Martin Davis said? Perhaps give a citation?
From: Charlie-Boo on 31 May 2010 13:18 On May 31, 6:12 am, Rupert <rupertmccal...(a)yahoo.com> wrote: > On May 30, 10:45 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > Everyone including Martin Davis (his anthology) says that Rosser 1936 > > can't be extended because an inconsistent system proves everything and > > so is complete (in a very bad way.) But Turing 1937 includes a > > derivation of Rosser 1936. So what are the possibilities? > > > 1. Turing 1937 is equivalent to Rosser 1936. > > > 2. Martin Davis and everybody else are wrong. > > > 3. They need to more closely examine the notion of extending a > > theorem. > > > 4. What? > > > C-B > > Perhaps I will have a look at Turing 1937 I have believed for years that Turing 1937 proves Rosser 1936 and also proves that the Entscheidungsproblem is unsolvable. Now I look at Turing 1937 and it doesnt seem to prove either! http://groups.google.com/group/sci.logic/browse_thread/thread/ea31026429087bff?hl=en Boy, I havent been this confused in a long time (several minutes at least.) Did Turing prove Rossers 1936 result?? > and see what I think. But > maybe you could tell us *exactly* what it is that Martin Davis said? > Perhaps give a citation? The Undecidable Edited by Martin Davis 1965 Raven Press Page 230 Dover reprint: http://www.amazon.com/Undecidable-Propositions-Unsolvable-Computable-Functions/dp/0486432289/ref=sr_1_1?ie=UTF8&s=books&qid=1275317240&sr=1-1 EXTENSIONS OF SOME THEOREMS OF GODEL AND CHURCH In this paper, Rosser shows that the assumption of w-consistency in Godels theorem (this anthology, pp. 23-26) can be replaced by simple consistency. Clearly this assumption can not be further weakened: if the system of logic being considered is inconsistent, then all of its assertions are theorems, and hence there is no undecidability. C-B
From: Rupert on 31 May 2010 18:42 On Jun 1, 3:18 am, Charlie-Boo <shymath...(a)gmail.com> wrote: > On May 31, 6:12 am, Rupert <rupertmccal...(a)yahoo.com> wrote: > > > > > > > On May 30, 10:45 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > > Everyone including Martin Davis (his anthology) says that Rosser 1936 > > > can't be extended because an inconsistent system proves everything and > > > so is complete (in a very bad way.) But Turing 1937 includes a > > > derivation of Rosser 1936. So what are the possibilities? > > > > 1. Turing 1937 is equivalent to Rosser 1936. > > > > 2. Martin Davis and everybody else are wrong. > > > > 3. They need to more closely examine the notion of extending a > > > theorem. > > > > 4. What? > > > > C-B > > > Perhaps I will have a look at Turing 1937 > > I have believed for years that Turing 1937 proves Rosser 1936 and also > proves that the Entscheidungsproblem is unsolvable. Now I look at > Turing 1937 and it doesnt seem to prove either! > > http://groups.google.com/group/sci.logic/browse_thread/thread/ea31026... > > Boy, I havent been this confused in a long time (several minutes at > least.) > > Did Turing prove Rossers 1936 result?? > I would imagine so. I would have to have a look at the paper. > > and see what I think. But > > maybe you could tell us *exactly* what it is that Martin Davis said? > > Perhaps give a citation? > > The Undecidable > Edited by Martin Davis > 1965 Raven Press > Page 230 > > Dover reprint: > > http://www.amazon.com/Undecidable-Propositions-Unsolvable-Computable-... > > EXTENSIONS OF SOME THEOREMS OF GODEL AND CHURCH In this paper, > Rosser shows that the assumption of w-consistency in Godels theorem > (this anthology, pp. 23-26) can be replaced by simple consistency. > Clearly this assumption can not be further weakened: if the system of > logic being considered is inconsistent, then all of its assertions are > theorems, and hence there is no undecidability. > Yes, well, there is nothing wrong with this statement. He is saying that the hypothesis of consistency cannot be weakened. I don't see how the fact that Turing gave an alternative proof poses a problem.
From: George Greene on 1 Jun 2010 15:13 On May 30, 8:45 am, Charlie-Boo <shymath...(a)gmail.com> wrote: > Everyone including Martin Davis (his anthology) says that Rosser 1936 > can't be extended because an inconsistent system proves everything and > so is complete (in a very bad way.) Davis is right. What is there to discuss?? > But Turing 1937 includes a > derivation of Rosser 1936. So? > So what are the possibilities? > > 1. Turing 1937 is equivalent to Rosser 1936. Well, it may not be exactly equivalent, but if he just derived what Rosser had already derived, where is the problem? Where is the conflict? There do not NEED to arise any "possibilities" out of this state of affairs! Davis, Rosser, and Turing all simply AGREE that you can improve on Godel's original proof by relaxing the requirement for w-consistency to simple consistency.
From: Charlie-Boo on 3 Jun 2010 22:47
On May 31, 6:42 pm, Rupert <rupertmccal...(a)yahoo.com> wrote: > On Jun 1, 3:18 am, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > > > > > On May 31, 6:12 am, Rupert <rupertmccal...(a)yahoo.com> wrote: > > > > On May 30, 10:45 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > > > Everyone including Martin Davis (his anthology) says that Rosser 1936 > > > > can't be extended because an inconsistent system proves everything and > > > > so is complete (in a very bad way.) But Turing 1937 includes a > > > > derivation of Rosser 1936. So what are the possibilities? > > > > > 1. Turing 1937 is equivalent to Rosser 1936. > > > > > 2. Martin Davis and everybody else are wrong. > > > > > 3. They need to more closely examine the notion of extending a > > > > theorem. > > > > > 4. What? > > > > > C-B > > > > Perhaps I will have a look at Turing 1937 > > > I have believed for years that Turing 1937 proves Rosser 1936 and also > > proves that the Entscheidungsproblem is unsolvable. Now I look at > > Turing 1937 and it doesnt seem to prove either! > > >http://groups.google.com/group/sci.logic/browse_thread/thread/ea31026... > > > Boy, I havent been this confused in a long time (several minutes at > > least.) > > > Did Turing prove Rossers 1936 result?? > > I would imagine so. I would have to have a look at the paper. > > > > > > > > and see what I think. But > > > maybe you could tell us *exactly* what it is that Martin Davis said? > > > Perhaps give a citation? > > > The Undecidable > > Edited by Martin Davis > > 1965 Raven Press > > Page 230 > > > Dover reprint: > > >http://www.amazon.com/Undecidable-Propositions-Unsolvable-Computable-... > > > EXTENSIONS OF SOME THEOREMS OF GODEL AND CHURCH In this paper, > > Rosser shows that the assumption of w-consistency in Godels theorem > > (this anthology, pp. 23-26) can be replaced by simple consistency. > > Clearly this assumption can not be further weakened: if the system of > > logic being considered is inconsistent, then all of its assertions are > > theorems, and hence there is no undecidability. > > Yes, well, there is nothing wrong with this statement. He is saying > that the hypothesis of consistency cannot be weakened. I don't see how > the fact that Turing gave an alternative proof poses a problem.- Hide quoted text - > > - Show quoted text -- Hide quoted text - > > - Show quoted text - Interesting that you characterize it as just another proof. If you prove a theorem using its various little premises, then if you can prove the premises from the theorem then you simply change the theorem from referring to "premises" or "sufficient condition" to referring to "necessary and sufficient." => becomes <=>. But if the premises are a big important theorem, then you have the interesting case that the new theorem is equivalent to the original theorem. And if you can't prove the premises from the theorem, then the premises are strictly stronger than the theorem. There are situations where information is given by the premises that is not given by the theorem. That too is more interesting if the theorem is seen as being as strong as possible. You somehow have something stronger. Applied to Rosser 1936 and Turing 1937, what do we get? Then I'll go further. But at some point we might need that proof of Rosser 1936 in Turing 1937 and at the present (as I say) I seem to have lost it! :( I remember Torkel [like Cher and Saddam!] asking what was so special about one of my proofs of Rosser 1936 by referring to Turing 1937, including reference to "recursively axiomatizable." C-B |