Związek twierdzeń o niekompletności Gödla z tezą Kościoła Turinga

To może być naiwne pytanie, ale proszę bardzo. (Edycja - nie ma głosów pozytywnych, ale nikt też nie odpowiedział; być może pytanie jest trudniejsze, niejasne lub niejasne, niż myślałem?)

Pierwsze twierdzenie Gödela o niekompletności można udowodnić jako następstwo nierozstrzygalności problemu zatrzymania (np. Sipser Ch. 6; post na blogu Scotta Aaronsona ).

Z tego, co rozumiem (potwierdzone komentarzami), dowód ten nie zależy od tezy Kościoła-Turinga. Wywodzimy się z tej sprzeczności, pokazując, że w kompletnym i spójnym systemie formalnym Maszyna Turinga mogłaby rozwiązać problem zatrzymania. (Gdybyśmy z drugiej strony pokazali, że jakaś skuteczna procedura może rozstrzygnąć problem zatrzymania, musielibyśmy również przyjąć tezę Turinga, aby uzyskać sprzeczność).

Można więc powiedzieć, że wynik ten zapewnia nieco intuicyjne poparcie dla tezy Kościoła-Turinga, ponieważ pokazuje, że ograniczenie Maszyn Turinga pociąga za sobą ograniczenie uniwersalne. (Post na blogu Aaronsona z pewnością popiera ten pogląd).

Moje pytanie brzmi: czy możemy uzyskać coś bardziej konkretnego, idąc w drugą stronę: Jakie formalne implikacje twierdzenia Gödela mają dla tezy o Kościele Turinga? Na przykład intuicyjnie wydaje się możliwe, że twierdzenie Pierwszej Niekompletności oznacza, że ​​żadna skuteczna procedura nie może ustalić, czy zatrzyma się dowolna Maszyna Turinga; rozumowanie może być takie, że istnienie takiej procedury implikuje zdolność do zbudowania pełnej spójnej teorii . Czy to jest poprawne? Czy są jakieś wyniki w tym zakresie?$\omega$

(Pytam z ciekawości - nie studiuję logiki - przepraszam, jeśli jest to dobrze znane, czy nie na poziomie badawczym. W takim przypadku rozważ to jako prośbę o referencje! Dziękujemy za wszelkie komentarze lub odpowiedzi !)

Pytanie, które wydaje się powiązane, ale nie jest takie: Twierdzenie Kościoła i Twierdzenia o niekompletności Gödla

EDYCJA: Spróbuję wyjaśnić pytanie! Po pierwsze - moją naiwną intuicją jest to, że niekompletność Gödela powinna implikować przynajmniej pewne ograniczenia tego, co jest lub nie jest obliczalne. Ograniczenia te byłyby bezwarunkowe, tzn . Powinny dotyczyć wszystkich modeli obliczeniowych, a nie tylko maszyn Turinga.

Zastanawiam się więc, czy tak jest w tym przypadku (muszą być jakieś implikacje, prawda?). Zakładając, że tak, jestem najbardziej ciekawy, jak wpływa to na tezę Turinga - pojęcie, że wszystko, co można skutecznie obliczyć, może być obliczone przez maszynę Turinga. Na przykład wydaje się możliwe, że istnienie skutecznej procedury decydowania o tym, czy maszyna Turinga zatrzyma się, byłoby sprzeczne z twierdzeniem o pierwszej niekompletności. Ten wynik pokazałby, że żadna możliwa metoda obliczeń nie może być „znacznie” mocniejsza niż Maszyny Turinga; ale czy ten wynik jest prawdziwy? Mam kilka podobnych pytań w komentarzach. Byłbym bardzo zainteresowany, aby usłyszeć odpowiedź na jedno z tych pytań, wskazówkę do odpowiedzi w literaturze, wyjaśnienie, dlaczego całe moje rozumowanie jest nieuzasadnione, lub jakiekolwiek inne komentarze!

Oto filozoficzna odpowiedź, która może cię zabawiać.

Twierdzenia Gödela o niekompletności dotyczą formalnego systemu arytmetyki Peano. Jako takie nie mówią nic o modelach obliczeniowych, przynajmniej nie bez pewnej interpretacji.

Arytmetyka Peano z łatwością pokazuje istnienie funkcji, które nie są obliczalne. Na przykład, będąc klasyczną teorią wystarczająco wyrazistą, aby mówić o maszynach Turinga, pokazuje szczególny przykład wykluczonego środka, który mówi, że każda maszyna Turinga zatrzymuje się lub działa na zawsze. Niemniej jednak z pracy Gödla powstało ważne pojęcie obliczalności, a mianowicie (prymitywna) funkcja rekurencyjna . Więc nie same twierdzenia łączą się z obliczalnością, ale raczej metoda dowodu, która je ustala.

Istotę twierdzeń o niekompletności można wyrazić w formie abstrakcyjnej przy użyciu logiki sprawdzalności, która jest rodzajem logiki modalnej. Daje to twierdzeniom o niekompletności szeroki zakres zastosowań znacznie wykraczający poza arytmetykę i obliczalność Peano. Gdy tylko pewne zasady punktu stałego zostaną spełnione, zaczyna się niekompletność. Te zasady punktu stałego są spełnione przez tradycyjną teorię obliczalności, która w związku z tym pada ofiarą niekompletności, przez co rozumiem istnienie nierozłącznych zestawów ce. Ponieważ możliwe do udowodnienia i obalające zdania arytmetyki Peano tworzą nierozdzielne zestawy ce, tradycyjne twierdzenia o niekompletności Gödla są w obliczeniach następstwem zjawisk niekompletności. (Jestem filozoficznie niejasny i twoja głowa będzie bolała, jeśli spróbujesz zrozumieć mnie jako matematyka).

Przypuszczam, że możemy zająć dwa stanowiska na temat tego, w jaki sposób wszystko to odnosi się do nieformalnego pojęcia skuteczności („rzeczy, które można faktycznie obliczyć”):

1. Z tego, co wiemy, jesteśmy po prostu dość skończonym automatem, zdolnym do rozważania fikcyjnych superbohaterów zwanych „maszynami Turinga”, które są w stanie obliczyć z nieograniczonymi liczbami (dysząc!). W takim przypadku Gödel był po prostu bardzo dobrym gawędziarzem. To, jak jego historie przekładają się na efektywność, jest więc kwestią pewnego (niekoniecznie niedokładnego) zastosowania wyobraźni do rzeczywistości.

2. Ponieważ zjawiska niekompletności powstają naturalnie w wielu kontekstach, a na pewno we wszystkich rozsądnych pojęciach obliczeniowych, dochodzimy do wniosku, że to samo musi dotyczyć skuteczności. Załóżmy na przykład, że moglibyśmy wysłać maszyny Turinga do czarnych dziur, aby obliczyć maszyny Turinga w nieskończonym czasie Joela Hamkina . To daje nam ogromną moc obliczeniową, w której wyrocznia zatrzymująca jest zabawką przedszkolną. Mimo to model spełnia podstawowe warunki, które pozwalają nam pokazać istnienie zbiorów możliwych do wstawienia. Dlatego po raz kolejny obliczenia nie są wszechpotężne, a niekompletność jest faktem.

Chciałbym podkreślić komentarz Neela , głównymi narzędziami zarówno nierozstrzygalności zatrzymania, jak i twierdzeń Godela o niekompletności są:

1. kodowanie pojęć składniowych, takich jak dowody, obliczenia itp., za pomocą liczb / łańcuchów i relacji / funkcji nad nimi;
2. Twierdzenie Godela o punkcie stałym.

Kodowanie obiektów i pojęć składniowych może dziś wydawać się oczywiste, że jesteśmy przyzwyczajeni do komputerów cyfrowych, ale jest to genialny pomysł niezbędny dla uniwersalnych komputerów i oprogramowania. Wszystko, co jest potrzebne do udowodnienia istnienia uniwersalnego symulatora, znajduje się w jego pracy.

Godel pokazuje również, że możemy reprezentować te pojęcia składniowe i ogólnie obliczalne relacje / funkcje TM za pomocą prostych wzorów arytmetycznych.

Krótko mówiąc, dowód niekompletności Godela jest następujący:

$T$

1. $Provable_T(x)$$T$$x$$T$
2. $G$$\lnot Provable(x)$$T \vdash G \leftrightarrow \lnot Provable_T(\ulcorner G \urcorner)$

Nierozstrzygalność problemu zatrzymania dla baz TM wykorzystuje podobne składniki:

1. $Halt(x)$$x$
2. $N$Ź H l t ( ⟨ M ⟩ $N$$\lnot Halt(\langle M \rangle)$

Nierozstrzygalność zatrzymania dla TM daje niekompletność, ponieważ możemy przedstawić w i możemy obliczalnie wyliczyć twierdzenia , a jeśli jest kompletny, możemy zdecydować, czy dana TM zatrzymuje się, czy nie, sprawdzając, czy odpowiedni wzór jest możliwy do udowodnienia w .T T T $Halt(x)$$T$$T$$T$$T$

Odwrotna sytuacja jest również prosta: jeśli teorią jest ce, to możliwość udowodnienia jest rozstrzygalna przy użyciu problemu zatrzymania, dlatego moglibyśmy zbudować kompletną teorię, dodając coraz więcej wzorów, których negacji nie da się udowodnić. Dlatego jeżeli zatrzymanie problemem było rozstrzygalne, wtedy możemy mieć pełną rozszerzenie CE .T $T$$T$$T$

Dowody są bardzo podobne i wykorzystują te same składniki (chociaż dla kogoś, kto jest bardziej zaznajomiony z bazami TM, ale nie ma zbytniej logiki, nierozstrzygalność problemu zatrzymania może wyglądać prostiej: szczególny przypadek twierdzenia o stałym punkcie zastosowany w dowodzie nierozstrzygalności może wyglądać prostiej niż szczególny przypadek punktu stałego zastosowanego w twierdzeniu Godela, chociaż są one zasadniczo takie same, ale podstawowymi ideami są po prostu kodowanie obiektów i pojęć składniowych z wykorzystaniem liczb / ciągów i wzorów / funkcji wokół nich oraz zastosowanie twierdzenia o punkcie stałym).

Myślę, że do twierdzeń można użyć mocniejszych modeli obliczeniowych, można obliczyć wracle oracle , rozważyć problem zatrzymania TM z dostępem do oracle i rozważyć arytmetykę, która ma predykat i aksjomaty definiujące wykres . Będziemy mieć podobną sytuację obliczalności względem .O P O ( x ) O $O$$O$$P_O(x)$$O$$O$

ps:
Należy zauważyć, że twierdzenia Godela zostały opublikowane w 1931 r., podczas gdy nierozstrzygalność Turinga została opublikowana w 1936 r. W momencie publikacji artykułu Godela TM nie zostały zdefiniowane, a Godel używał innego równoważnego modelu. IIRC, Godel nie był w pełni zadowolony ze swojego wyniku, jakim było ustalenie pierwotnego celu programu Hilberta, ponieważ nie był przekonany, że zastosowany model obliczeń naprawdę uchwycił intuicyjne pojęcie obliczeń algorytmicznych, był zadowolony tylko po filozoficznym sporze Turinga o przechwytywaniu TM intuicyjne pojęcie obliczalności algorytmicznej. Myślę, że możesz przeczytać więcej na ten temat w zebranych pracach Godela.