Unsolvability of the Entscheidungsproblem as a Corollary of Gödel’s 2nd Theorem
in [Math]
|
Prev: Redshift and Microwave radiation favor Atom Totality and disfavor Big Bang #117; ATOM TOTALITY (Atom Universe) theory; replaces Big Bang theory
Next: online computation of semiconvergents?
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: Charlie-Boo on 4 Jun 2010 00:06
On May 31, 6:35 pm, Rupert <rupertmccal...(a)yahoo.com> wrote: > 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. Not so. If a set is recursive then there is a wff that represents it and whose negation represents its complement. That might be called "defines" by some. C-B > > > > So dont we have a proof that is (1) way simpler, and (2) way earlier, > > than Church and Turing? > > > C-B- Hide quoted text - > > - Show quoted text -- Hide quoted text - > > - Show quoted text - |