Twierdzenie Kościoła i twierdzenia o niekompletności Gödla

Niedawno czytałem o niektórych pomysłach i historii przełomowej pracy wykonanej przez różnych logików i matematyków w zakresie obliczeń. Podczas gdy poszczególne koncepcje są dla mnie dość jasne, staram się dobrze zrozumieć wzajemne relacje i abstrakcyjny poziom, na którym wszystkie są ze sobą powiązane.

Wiemy, że twierdzenie Kościoła (a raczej niezależne dowody Entscheidungsproblem Hilberta autorstwa Alonza Churcha i Alana Turinga) udowodniły, że ogólnie nie jesteśmy w stanie obliczyć, czy dane stwierdzenie matematyczne w systemie formalnym jest prawdziwe, czy fałszywe. Jak rozumiem, teza Churcha-Turinga zapewnia dość jasny opis równoważności (izomorfizmu) między rachunkiem lambda Kościoła a maszynami Turinga, dlatego faktycznie mamy ujednolicony model obliczalności. (Uwaga: O ile mi wiadomo, dowód Turinga wykorzystuje fakt, że problem zatrzymania jest nierozstrzygalny. Popraw mnie, jeśli się mylę.)

Otóż ​​pierwsze twierdzenie Gödela o niekompletności stwierdza, że ​​nie wszystkie stwierdzenia w spójnym systemie formalnym o wystarczającej mocy arytmetycznej mogą być udowodnione lub obalone (rozstrzygnięte) w tym systemie. Pod wieloma względami wydaje mi się, że mówi to dokładnie to samo, co twierdzenia Kościoła, biorąc pod uwagę, że rachunek lambda i maszyny tokarskie są skutecznie formalnymi rodzajami systemów!

Jest to jednak moja całościowa interpretacja i miałem nadzieję, że ktoś rzuci nieco światła na szczegóły. Czy te dwa twierdzenia są faktycznie równoważne? Czy są jakieś subtelności, których należy przestrzegać? Jeśli te teorie zasadniczo patrzą na tę samą uniwersalną prawdę na różne sposoby, dlaczego podchodzi się do nich z tak różnych perspektyw? (Minęło mniej więcej 6 lat między dowodem Godela a dowodem Kościoła). Wreszcie, czy możemy zasadnie powiedzieć, że koncepcja sprawdzalności w systemie formalnym (rachunek dowodowy) jest identyczna z koncepcją obliczalności w teorii rekurencji (maszyny Turinga / rachunek lambda)?

Po pierwsze, sugeruję przeczytanie „Metamatematyki” Kleene'a jako dobrej książki na te tematy. Dwa pierwsze rozdziały tomu I „Klasycznej teorii rekurencji” Odifreddiego również mogą być pomocne w zrozumieniu związku między tymi pojęciami.

Wiemy, że twierdzenie Kościoła (a raczej niezależne dowody Entscheidungsproblem Hilberta autorstwa Alonza Churcha i Alana Turinga) udowodniły, że ogólnie nie jesteśmy w stanie obliczyć, czy dane stwierdzenie matematyczne w systemie formalnym jest prawdziwe, czy fałszywe.

Myślę, że odwołujesz się do twierdzenia Kościoła, że ​​zbiór twierdzeń logiki pierwszego rzędu nie jest rozstrzygalny. Ważne jest, aby pamiętać, że język jest pierwszym rzędem.

Jak rozumiem, teza Churcha-Turinga zapewnia dość jasny opis równoważności (izomorfizmu) między rachunkiem lambda Kościoła a maszynami Turinga, dlatego skutecznie dysponujemy ujednoliconym modelem obliczalności.

Nie. Równoważność obliczalności lambda i Turinga jest twierdzeniem Kleene'a. To nie jest teza. Uważany jest za dowód na poparcie tezy Kościoła.

Uwaga: O ile mi wiadomo, dowód Turinga wykorzystuje fakt, że problem zatrzymania jest nierozstrzygalny. Popraw mnie, jeśli się mylę.

Otóż ​​pierwsze twierdzenie Gödela o niekompletności stwierdza, że ​​nie wszystkie twierdzenia w spójnym systemie formalnym mogą zostać udowodnione w tym systemie. Pod wieloma względami wydaje mi się, że mówi to dokładnie to samo, co twierdzenia Kościoła, biorąc pod uwagę, że rachunek lambda i maszyny tokarskie są skutecznie formalnymi rodzajami systemów!

$\omega$$\varphi$$\varphi$$\lnot \varphi$

To nie oznacza tego samego. Nic nie mówi o tym, że zestaw twierdzeń teorii jest nierozstrzygalny.

Jest to jednak moja całościowa interpretacja i miałem nadzieję, że ktoś rzuci nieco światła na szczegóły. Czy te dwa twierdzenia są faktycznie równoważne? Czy są jakieś subtelności, których należy przestrzegać? Jeśli te teorie zasadniczo patrzą na tę samą uniwersalną prawdę na różne sposoby, dlaczego podchodzi się do nich z tak różnych perspektyw? (Minęło mniej więcej 6 lat między dowodem Godela a dowodem Kościoła).

Przez lata było wiele nadużyć twierdzeń Godela (i podobnych twierdzeń). Należy być bardzo ostrożnym, dokonując ich interpretacji. O ile widziałem, nadużycia są zwykle wynikiem zapomnienia o podaniu pewnego warunku w twierdzeniu lub połączenia twierdzeń z innymi przekonaniami. Uważne spojrzenie pokazuje, że tezy, choć powiązane, nie są równoważne.

Wreszcie, czy możemy zasadnie powiedzieć, że koncepcja sprawdzalności w systemie formalnym (rachunek dowodowy) jest identyczna z koncepcją obliczalności w teorii rekurencji (maszyny Turinga / rachunek lambda)?

Nie rozumiem, co rozumiesz przez „identyczny”. Z pewnością istnieje wiele zależności między obliczalnością a sprawdzalnością. Mogę być w stanie przedstawić bardziej pomocny komentarz, jeśli wyjaśnisz, co masz na myśli, mówiąc, że są identyczne.

aktualizacja

$L$$T$$Thm(T)$$T$$\lnot Thm(T)$$T$$True$$False$$True$$False$$L = True \cup False$

$Thm(T) \cup \lnot Thm(T)$$L$$T$

$Thm(T)$$Thm(T)$

O związku między sprawdzalnością w systemie formalnym a obliczalnością. Jedna z nich jest następująca: jeśli system jest skuteczny, to zestaw wyrażeń pochodnych w nim jest re, a układ jest szczególnym przypadkiem gramatyki. Gramatyki to kolejny sposób definiowania pojęcia obliczalności, który jest równoważny z obliczalnością maszyny Turinga.

czy możemy zasadnie powiedzieć, że koncepcja sprawdzalności w systemie formalnym (rachunek dowodowy) jest identyczna z koncepcją obliczalności w teorii rekurencji (maszyny Turinga / rachunek lambda)?

Są one bardzo podobne, ale nie identyczne, ponieważ niektóre etapy rachunku próbnego mogą reprezentować operacje niepoliczalne.

$ZFC$$\wp(N)$

Podobnie, twierdzenie Gödela o kompletności mówi nam, że jakakolwiek poprawna formuła w logice pierwszego rzędu ma dowód, ale twierdzenie Trakhtenbrota mówi nam, że w przypadku modeli skończonych ważność formuł pierwszego rzędu jest niezdecydowana.

Skończone dowody niekoniecznie odpowiadają operacjom obliczalnym.

Chociaż nie jest to do końca to, o co pytasz, jest w tym samym stylu i mam nadzieję, że ty (i inni czytelnicy twojego pytania) zainteresuje cię. Zdecydowanie powinieneś przeczytać o korespondencji Curry-Howarda , która mówi, że kategoria programów jest w pewnym sensie izomorficzna w stosunku do kategorii konstruktywnych dowodów. (Omówiono dowody i obliczalność na innym poziomie niż inne odpowiedzi).

Spróbuję odpowiedzieć na twoje pytanie w skrócie; Próbuję też odnieść te dwa twierdzenia w inny sposób.

Pierwsze twierdzenie Gödela o niekompletności stwierdza, że ​​w spójnym systemie formalnym o wystarczającej mocy arytmetycznej istnieje stwierdzenie P, które nie dowodzi ani jego, ani jego negacji. Nie oznacza to, że nie istnieje algorytm decyzyjny dla zestawu twierdzeń teorii, który powiedziałby również, że ani P, ani P nie są twierdzeniami. Wynik twierdzenia Church-Turinga mówi, że taki algorytm nie istnieje. To także sedno odpowiedzi Kaveha, mam nadzieję, że wyjaśniłem to jaśniej.

Spróbuję teraz udowodnić, że twierdzenie Church-Turinga sugeruje twierdzenie Gödla, proszę wyjaśnij mi, gdzie i jeśli się mylę. Zbiór twierdzeń Thm jest częściowo rozstrzygalny i przypuśćmy, że R jest programem, który rozpoznaje go (tzn. Zatrzymuje się na „tak”, jeśli wejście jest w Thm, dalej działa inaczej). Wykorzystajmy to do zbudowania nowego algorytmu: biorąc pod uwagę instrukcję Q, aby sprawdzić, czy jest to możliwe, uruchom R równolegle na Q, a nie Q, przeplatając ich wykonanie i zatrzymując się, gdy pierwszy z nich się zatrzyma, i produkując „Nie”, jeśli udowodniono „nie Q”, a w przeciwnym razie „Tak”; daje to algorytm obliczalny. Zakładając sprzeczność, że wszystkie twierdzenia można udowodnić lub obalić, algorytm ten rozwiązałby Entscheidungsproblem, ale to absurd! Dlatego musi istnieć stwierdzenie, które może „