Tjuringov dokaz

Tjuringov dokaz je dokaz Alana Tjuringa, prvi put objavljen u novembru 1936. pod naslovom „O izračunljivim brojevima, sa primenom na Entscheidungsproblem“. Bio je to drugi dokaz (posle Čerčeve teoreme) negacije Hilbertovog Entscheidungsproblem; to jest, pretpostavke da se na neka čisto matematička da-ne pitanja nikada ne može odgovoriti računanjem; tehnički gledano, da su neki problemi odlučivanja „neodlučivi” u smislu da ne postoji jedinstveni algoritam koji nepogrešivo daje tačan „da” ili „ne” odgovor na svaku instancu problema. Tjuringovim sopstvenim rečima: „ono što ću dokazati je sasvim drugačije od dobro poznatih Gedelovih rezultata... Sada ću pokazati da ne postoji opšta metoda koja govori da li je data formula U dokaziva u K [Principia Mathematica]“.

Tjuring je pratio ovaj dokaz sa još dva druga. Drugi i treći se oslanjaju na prvi. Svi se oslanjaju na njegov razvoj „računarskih mašina“ sličnih pisaćim mašinama koje se povinjavaju jednostavnom skupu pravila i na njegov kasniji razvoj „univerzalne računarske mašine“.

Sažetak dokaza

U svom dokazu da problem odluke može biti bez rešenja, Tjuring je pošao od dva dokaza koji su trebali da dovedu do njegovog konačnog dokaza. Njegova prva teorema je najrelevantnija za problem zaustavljanja, druga je relevantnija za Rajsovu teoremu.

Prvi dokaz: da ne postoji „računarska mašina“ koja može odlučiti da li je proizvoljna „računarska mašina“ (kao što je predstavljena celim brojem 1, 2, 3, . . .) „bez kruga“ (tj. nastavlja da štampa svoj broj u binarnom obliku ad infinitum): „...nemamo opšti proces da to uradimo u konačnom broju koraka“ (str. 132, ibid.). Tjuringov dokaz, iako se čini da koristi „dijagonalni proces“, u stvari pokazuje da njegova mašina (nazvana H) ne može da izračuna sopstveni broj, a kamoli ceo dijagonalni broj (Kantorov dijagonalni argument): „Zabluda u argumentu leži u pretpostavka da je B [dijagonalni broj] izračunljiv“ Dokaz ne zahteva mnogo matematike.

Drugi dokaz: Ovaj je čitaocima možda poznatiji kao Rajsova teorema: „Možemo dalje pokazati da ne može postojati mašina E koja će, kada je snabdevena S.D [„programom“] proizvoljne mašine M, odrediti da li će M ikada štampa dati simbol (recimo 0)”

Treći dokaz: „Odgovarajući svakoj računarskoj mašini M konstruišemo formulu Un(M) i pokazujemo da, ako postoji opšti metod za određivanje da li je Un(M) dokazivo, onda postoji opšti metod za određivanje da li M ikada štampa 0”.

Treći dokaz zahteva upotrebu formalne logike za dokazivanje prve leme, nakon čega sledi kratak dokaz druge rečima:

Lema 1: Ako se S1 [simbol „0”] pojavi na traci u nekoj potpunoj konfiguraciji M, onda je Un(M) dokazivo.
Lema 2: [Obratno] Ako je Un(M) dokazivo onda se S1 [simbol „0”] pojavljuje na traci u nekoj potpunoj konfiguraciji M.

Konačno, u samo 64 reči i simbola Tjuring dokazuje reductio ad absurdum da „Hilbertov problem odluke može imati rešenje“.

Literatura

• Davis, Martin (1965). The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions. New York: Raven Press.  The two papers of Post referenced above are included in this volume. Other papers include those by Gödel, Church, Rosser, and Kleene.
  • Davis, Martin (2004). The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions. Dover. ISBN 9780486432281. 
• Franzén, Torkel (2005). Gödel's Theorem: An Incomplete Guide to its Use and Abuse. A K Peters. 
• Hodges, Andrew (1983). Alan Turing: The Enigma. New York: Simon and Schuster.  Cf. Chapter "The Spirit of Truth" for a history leading to, and a discussion of, his proof.
• Reichenbach, Hans (1947). Elements of Symbolic Logic. New York: Dover Publications, Inc. 
• Turing, A.M. (1937). „On Computable Numbers, with an Application to the Entscheidungsproblem”. Proceedings of the London Mathematical Society. 2. 42 (1): 230—65. S2CID 73712. doi:10.1112/plms/s2-42.1.230. 
• Turing, A.M. (1938). „On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction”. Proceedings of the London Mathematical Society. 2. 43 (6): 544—6. doi:10.1112/plms/s2-43.6.544.  This is the epochal paper where Turing defines Turing machines, shows that the Entscheidungsproblem is unsolvable.