Did Turing 1937 Really Prove the Entscheidungsproblem Unsolvable?
in [Logic]
|
Prev: Unsolvability of the Entscheidungsproblem as a Corollary of Gödel’s 2nd Theorem
Next: [FAQ, 06/11/05] Mathematical logic on the web
From: Charlie-Boo on 3 Jun 2010 23:15 On May 31, 6:32 pm, Rupert <rupertmccal...(a)yahoo.com> wrote: > On Jun 1, 2:58 am, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > > > > > Excerpt from Turing 1937: > > > 11. Application to the Entscheidungsproblem. > > > The results of §8 have some important applications. In particular, > > they can be used to show that the Hilbert Entscheidungsproblem can > > have no solution. For the present I shall confine myself to proving > > this particular theorem. > > > I propose, therefore, to show that there can be no general process for > > determining whether a given formula U of the functional calculus Z is > > provable, i.e. that there can be no machine which, supplied with any > > one U of these formulae, will eventually say whether U is provable. > > > If the negation of what Gödel has shown had been proved, i.e. if, for > > each U, either U or U is provable, then we should have an immediate > > solution of the Entscheidungsproblem. For we can invent a machine K > > which will prove consecutively all provable formulae. Sooner or later > > K will reach either U or U. If it reaches U, then we know that U is > > provable. If it reaches U, then, since Z is consistent (Hilbert and > > Ackermann, p.65), we know that U is not provable. > > > Owing to the absence of integers in Z the proofs appear somewhat > > lengthy. The underlying ideas are quite straightforward. > > > But that only proves that if Godels 1st. Theorem were false then the > > Entscheidungsproblem would be solvable. The fact that Godels 1st. > > Theorem is true does not infer anything here. Where does Turing prove > > that the Entscheidungsproblem is unsolvable? > > I would imagine he does so in the rest of the paper... > > Do you want me to go and have a look for you?- Hide quoted text - > > - Show quoted text - Yes! Accept the challenge. C-B
From: Charlie-Boo on 3 Jun 2010 23:38 On May 31, 6:32 pm, Rupert <rupertmccal...(a)yahoo.com> wrote: > On Jun 1, 2:58 am, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > > > > > Excerpt from Turing 1937: > > > 11. Application to the Entscheidungsproblem. > > > The results of §8 have some important applications. In particular, > > they can be used to show that the Hilbert Entscheidungsproblem can > > have no solution. For the present I shall confine myself to proving > > this particular theorem. > > > I propose, therefore, to show that there can be no general process for > > determining whether a given formula U of the functional calculus Z is > > provable, i.e. that there can be no machine which, supplied with any > > one U of these formulae, will eventually say whether U is provable. > > > If the negation of what Gödel has shown had been proved, i.e. if, for > > each U, either U or U is provable, then we should have an immediate > > solution of the Entscheidungsproblem. For we can invent a machine K > > which will prove consecutively all provable formulae. Sooner or later > > K will reach either U or U. If it reaches U, then we know that U is > > provable. If it reaches U, then, since Z is consistent (Hilbert and > > Ackermann, p.65), we know that U is not provable. > > > Owing to the absence of integers in Z the proofs appear somewhat > > lengthy. The underlying ideas are quite straightforward. > > > But that only proves that if Godels 1st. Theorem were false then the > > Entscheidungsproblem would be solvable. The fact that Godels 1st. > > Theorem is true does not infer anything here. Where does Turing prove > > that the Entscheidungsproblem is unsolvable? > > I would imagine he does so in the rest of the paper... > > Do you want me to go and have a look for you?- Hide quoted text - Go for it! I think he reduces Entscheidungsproblem to HP a few pages later. (I am sure that I could give a much simpler proof than he does.) Still looking for Rosser 1936. C-B > - Show quoted text -
From: Aatu Koskensilta on 4 Jun 2010 10:31
Charlie-Boo <shymathguy(a)gmail.com> writes: > I thought I saw it years ago. So you see it too? Just read Section 11. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus |