Dowód Turinga: Różnice pomiędzy wersjami
| [wersja przejrzana] | [wersja przejrzana] |
Usunięta treść Dodana treść
jęz. |
lin. |
||
Linia 7:
W 1931 [[Kurt Gödel]] pokazał, że system dowodzenia twierdzeń arytmetycznych sformalizowany w ramach [[Principia Mathematica]] nie jest zupełny i niesprzeczny. [[Twierdzenie Gödla|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 Church|Alonzo Churcha'a]] w 1936 i niezależną od niej, opublikowaną rok później, wyżej wspomnianą pracą [[Alan Turing|Alana Turinga]]. Church przedstawił dowód w ramach rozwijanego przez siebie formalizmu [[rachunek lambda|rachunku lambda]]. Turing posłużył się wprowadzoną przez siebie koncepcją [[maszyna Turinga|maszyny Turinga]]. Formalizmy te, jak się okazało, są równoważne {{odn|Turing|1937|s=231}}{{odn|Turing|1937|s=263}}, jednak wersja dowodu przedstawiona przez Turinga zyskała większą popularność.
W 1970 roku [[Yuri Matiyasevich]] udowodnił silniejsze twierdzenie dotyczące [[równanie diofantyczne|równań diofantycznych]], które m.in. implikuje wyniki Churcha i Turinga (patrz: [[dziesiąty problem Hilberta]]).
| |||