Dowód Turinga – dowód przedstawiony przez Alana Turinga w 1937 w pracy "On Computable Numbers, With an Application to the Entscheidungsproblem" pokazujący, że pewne ogólne klasy problemów są nierozstrzygalne, to znaczy nie istnieje uniwersalny algorytm rozwiązujący każdą instancje problemów z tych klas. W szczególności dowód daje negatywną odpowiedź na Entscheidungsproblem^[1].

W 1928 David Hilbert przedstawił problem decyzyjny (Entscheidungsproblem) dotyczący teorii aksjomatycznych logiki pierwszego rzędu, który można wyrazić następująco: podać algorytm rozstrzygający w skończonej liczbie kroków czy dla danego zbioru aksjomatów NT logiki pierwszego rzędu, zdanie T jest prawdziwe (czy T jest prawdziwe w każdym modelu spełniającym aksjomaty NT). Na mocy udowodnionego rok później twierdzenia Gödla o zupełności tak postawiony problem jest równoważny pytaniu czy zdanie T może zostać dedukcyjnie wyprowadzone z aksjomatów NT (patrz: dedukcja naturalna, system Hilberta).

W 1931 Kurt Gödel pokazał, że system dowodzenia twierdzeń arytmetycznych sformalizowany w ramach Principia Mathematica nie jest zupełny i niesprzeczny. Dowód Gödla jest czysto logiczny i nie odnosi się do żadnej notacji obliczalności, w związku z tym nie implikuje bezpośrednio nierozstrzygalności w obrębie zdań systemów aksjomatycznych logiki pierwszego rzędu.

Formalnie, negatywna odpowiedź na Entscheidungsproblem pojawiła się wraz z pracą Alonzo Churcha'a w 1936 i niezależną od niej, opublikowaną rok później, wyżej wspomnianą pracą Alana Turinga. Church przedstawił dowód w ramach rozwijanego przez siebie formalizmu rachunku lambda. Turing posłużył się wprowadzoną przez siebie koncepcją maszyny Turinga. Formalizmy te, jak się okazało, są równoważne^[1][2], jednak wersja dowodu przedstawiona przez Turinga zyskała większą popularność.

W 1970 roku Yuri Matiyasevich udowodnił silniejsze twierdzenie dotyczące równań diofantycznych, które m.in. implikuje wyniki Churcha i Turinga (patrz: dziesiąty problem Hilberta).

Dowód, że Entscheidungsproblem nie ma rozwiązania (lemat 3), stanowi wniosek w pracy Turinga wynikający z dwóch wcześniejszych lematów. Pierwszy lemat ma bliski związek z problemem stopu, drugi z twierdzeniem Rice’a.

Lemat 1 mówi, że nie istnieje maszyna Turinga, zdolna rozstrzygnąć w skończonej liczbie kroków czy dowolna maszyna Turinga jest "circle-free"^[3]. Dana maszyna jest "circle-free" jeżeli nie istnieje górne, skończone ograniczenie na liczbę symboli zerowych lub niezerowych, które generuje maszyna (np. maszyna, która kończy pracę nie jest "circle-free")^[4].

Lemat 2 mówi, że nie istnieje maszyna Turinga, która jest w stanie rozstrzygnąć w skończonej liczbie kroków czy dana maszyna Turinga generuje kiedykolwiek określony symbol (np. symbol zerowy). Jeżeliby tak było, prowadziłoby to do sprzeczności z lematem 1^[5].

Lemat 3 mówi, że odpowiednio dla każdej maszyny Turinga M można skonstruować formułę Un(M) i nie istnieje ogólny, mechaniczny proces (maszyna Turinga) rozstrzygający czy Un(M) jest dowodliwe. Jeżeliby tak było, prowadziłoby to do sprzeczności z lematem 2^[6].

Turing napisał: "Warto zaznaczyć, że to ... różni się od dobrze znanych wyników Gödla. Gödel pokazał, że (w formalizmie Principia Mathematica) istnieją twierdzenia T takie, że ani T ani ~T nie jest dowodliwe. Ja ... pokazuję, że nie istnieje ogólna (mechaniczna) metoda, która pozwala sprawdzić czy dana formuła T jest dowodliwa..."^[6].

• Twierdzenie Gödla

• Alan Turing. On Computable Numbers, With an Application to the Entscheidungsproblem. „Proceedings of the London Mathematical Society”. 42 (1), s. 230–265, 1937. DOI: 10.1112/plms/s2-42.1.230.