Unsolvability of the Entscheidungsproblem as a Corollary of Gödel’s 2nd Theorem
in [Logic]
|
Prev: Can Rosser 1936 be Extended? Alan Turing vs. Martin Davis et. al.
Next: Did Turing 1937 Really Prove the Entscheidungsproblem Unsolvable?
From: Charlie-Boo on 31 May 2010 12:27 Wikipedia: In 1936 and 1937 Alonzo Church and Alan Turing respectively, published independent papers showing that it is impossible to decide algorithmically whether statements in arithmetic are true or false, and thus a general solution to the Entscheidungsproblem is impossible. Alonzo Church, A note on the Entscheidungsproblem, Journal of Symbolic Logic, 1 (1936), pp 4041 Alan Turing, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, Series 2, 42 (1937), pp 230265 However, if the Entscheidungsproblem were solvable, then we could determine (and thus prove) whether the system is consistent by asking whether the sentence 0=1 is provable, as provability is expressible. So dont we have a proof that is (1) way simpler, and (2) way earlier, than Church and Turing? C-B
From: Rupert on 31 May 2010 18:35 On Jun 1, 2:27 am, Charlie-Boo <shymath...(a)gmail.com> wrote: > Wikipedia: > > In 1936 and 1937 Alonzo Church and Alan Turing respectively, > published independent papers showing that it is impossible to decide > algorithmically whether statements in arithmetic are true or false, > and thus a general solution to the Entscheidungsproblem is impossible. > > Alonzo Church, A note on the Entscheidungsproblem, Journal of > Symbolic Logic, 1 (1936), pp 4041 > > Alan Turing, On computable numbers, with an application to the > Entscheidungsproblem, Proceedings of the London Mathematical Society, > Series 2, 42 (1937), pp 230265 > > However, if the Entscheidungsproblem were solvable, then we could > determine (and thus prove) whether the system is consistent by asking > whether the sentence 0=1 is provable, as provability is expressible. > If the Entschiedungsproblem were solvable then you could determine whether PA is consistent. But it doesn't necessarily follow that you would be able to prove that PA is consistent in PA. Solving the Entscheidungsproblem just means you have an algorithm for answering the question, it doesn't say anything about supplying a proof in some theory T of the answer. > So dont we have a proof that is (1) way simpler, and (2) way earlier, > than Church and Turing? > > C-B
From: George Greene on 1 Jun 2010 15:18 On May 31, 12:27 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > Alonzo Church, A note on the Entscheidungsproblem, Journal of > Symbolic Logic, 1 (1936), pp 4041 > > Alan Turing, On computable numbers, with an application to the > Entscheidungsproblem, Proceedings of the London Mathematical Society, > Series 2, 42 (1937), pp 230265 > > However, if the Entscheidungsproblem were solvable, then we could > determine (and thus prove) whether the system is consistent by asking > whether the sentence 0=1 is provable, as provability is expressible. > > So dont we have a proof that is (1) way simpler, and (2) way earlier, > than Church and Turing? Why do you say "So" ?? "So" implies that something is following from some prior result. Where is your prior result? Who simply showed that the Eproblem was unsovlable PRIOR to this??
From: George Greene on 1 Jun 2010 15:19 On May 31, 6:35 pm, Rupert <rupertmccal...(a)yahoo.com> wrote: > If the Entschiedungsproblem were solvable then you could determine > whether PA is consistent. But it doesn't necessarily follow that you > would be able to prove that PA is consistent in PA. Solving the > Entscheidungsproblem just means you have an algorithm for answering > the question, it doesn't say anything about supplying a proof in some > theory T of the answer. The question said, "since provability is expressible". Is provability in PA "expressible" in PA ??
From: George Greene on 2 Jun 2010 18:37
On Jun 1, 3:29 pm, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote: > George Greene <gree...(a)email.unc.edu> writes: > > The question said, "since provability is expressible". Is provability > > in PA "expressible" in PA ?? > > Sure. That strikes me as a loose usage. It is NOT, as DMC was saying, "strongly representable", because you can't prove (in PA) the existence of even ONE thing that is UNprovable in PA, There are a lot of provability questions that PA doesn't decide one way or the other. In fact, even where PA proves X, which also entails&constitutes proving that X is provable, that still doesn't prove that ~X isn't ALSO provable (even though it isn't). This is not what natural- (as opposed to technical-) language speakers are going to mean by "expressible". More to the point, the actual provability-predicate that ALLEGEDLY DOES "express" provability-in-PA actually GETS IT WRONG in non-standard models of (e.g.) PA+~G. I liked "definable" better. |