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 31 May 2010 12:58 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? C-B
From: Frederick Williams on 31 May 2010 14:42 Charlie-Boo wrote: > > [...] The fact that Godel�s 1st. > Theorem is true does not infer anything here. You mean 'imply'. -- I can't go on, I'll go on.
From: Rupert on 31 May 2010 18:32 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?
From: Aatu Koskensilta on 1 Jun 2010 16:08 Charlie-Boo <shymathguy(a)gmail.com> writes: > Where does Turing prove that the Entscheidungsproblem is unsolvable? In a famous paper. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Charlie-Boo on 3 Jun 2010 23:14
On Jun 1, 4:08 pm, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote: > Charlie-Boo <shymath...(a)gmail.com> writes: > > Where does Turing prove that the Entscheidungsproblem is unsolvable? > > In a famous paper. I thought I saw it years ago. So you see it too? Ok, we'll all have a race to see who can find it the fastest. Where is it??? 11:13 P EST C-B > -- > Aatu Koskensilta (aatu.koskensi...(a)uta.fi) > > "Wovon man nicht sprechan kann, dar ber muss man schweigen" > - Ludwig Wittgenstein, Tractatus Logico-Philosophicus |