Undecidable problem

rdf:langString Problem nierozstrzygalny

rdf:langString Problem nierozstrzygalny – problem decyzyjny, dla którego nie istnieje algorytm, który po skończonej liczbie kroków i dla dowolnych danych wejściowych jednoznacznie odpowie tak lub nie. Turing w 1936 roku wykazał, że udzielenie odpowiedzi na pytanie, czy maszyna Turinga o numerze wykonując działania nad liczbą zakończy kiedyś swoją pracę, czy też przewidziany dla niej algorytm będzie realizowany w nieskończoność, jest problemem nierozstrzygalnym (patrz: problem stopu). Innym przykładem problemu nierozstrzygalnego jest tzw. zdanie Gödla o postaci 17 Gen r (generalizacja {kwantyfikator ogólny} formuły r względem zmiennej z numerem 17). Jest to zdanie posiadające tę własność, że ani ono, ani jego negacja nie dają się formalnie dowieść. Zdanie nierozstrzygalne powstało w wyniku odwzorowania antynomii logicznej (zwanej antynomią Richarda) poprzez tak zwaną arytmetyzacją języka klasycznego rachunku zdań. Arytmetyzacja języka pozwala na odwzorowanie relacji logicznych jakie zachodzą między zdaniami w relacje arytmetyczne między liczbami stanowiącymi numery tych zdań. Dzięki temu zamiast o relacjach logicznych można mówić o relacjach arytmetycznych. Istnienie zdania 17 gen r jest powodem nierozstrzygalności arytmetyki, uważanej do czasów Gödla za system rozstrzygalny, to znaczy taki, w którym prawdziwość każdego twierdzenia można rozstrzygnąć w oparciu o skończony zbiór kryteriów. Inaczej mówiąc, zbiór twierdzeń arytmetycznych jest nieobliczalny, co znaczy, że nie można w skończonej ilości kroków rozstrzygnąć, czy dany element tego zbioru, będący twierdzeniem arytmetycznym, jest, czy nie jest elementem zbioru twierdzeń. Tymczasem zbiór dowodów systemu formalnego jest obliczalny, ponieważ w skończonej ilości kroków można rozstrzygnąć, czy dany ciąg napisów jest, czy nie jest dowodem danego twierdzenia. Tak więc zbiór zdań prawdziwych nie pokrywa się ze zbiorem twierdzeń dowodzonych przez system. Wiemy bowiem, że istnieją zdania prawdziwe, których nie da się dowieść w tym systemie. Jednym z nich jest właśnie zdanie 17 Gen r.