Czy Edward Nelson przyjął twierdzenia o niezupełności?
Edward Nelson opowiadał się za słabymi wersjami arytmetyki (zwanymi arytmetyką predykatywną), które nie mogły udowodnić całości potęgowania. Ponieważ jego teoria rozszerza arytmetykę Robinsona, odnoszą się do niej twierdzenia o niezupełności. Ale jeśli twierdzenia o niekompletności zostaną udowodnione w teoriach silniejszych niż te, które przyjmuje, prawdopodobnie mógłby je odrzucić. Więc moje pytania są pierwsze: czy Nelson wątpił w którekolwiek z twierdzeń o niekompletności? Po drugie, czy twierdzenia o niezupełności można udowodnić w słabych systemach arytmetycznych, które nie dowodzą całości potęgowania?
Najbliższą odpowiedzią, jaką mogę znaleźć, jest fragment jego książki Predicative Arithmetic, w której na stronie 81 stwierdza, że „co najmniej jeden z tych dwóch filarów finitarnej logiki matematycznej, twierdzenie Hilberta-Ackermanna o spójności i drugie twierdzenie Gödla, sprawia, że odwołanie się do impredykatywnych koncepcji ”.
Odpowiedzi
Drugie twierdzenie Gödla o niekompletności nie wymaga ani potęgowania, ani „pojęć impredykatywnych”. Systemy, w których pracuje Nelson, to fragmenty arytmetyki, które można zinterpretować na definiowalnych cięciach$Q$; jednym takim fragmentem jest ograniczona arytmetyka$I\Delta_0+\Omega_1$ (wydaje się, że tak nazywa się Nelson $Q_4$w Predicative arytmetyce ). Teoria$I\Delta_0+\Omega_1$ (a nawet jego słabe fragmenty z bardziej ograniczoną indukcją, np $PV_1$) doskonale nadaje się do udowodnienia drugiego twierdzenia o niezupełności (dla teorii z zestawem aksjomatów w czasie wielomianowym, który nie jest rzeczywistym ograniczeniem).
( EDYCJA: zasadniczo przepisałem tę odpowiedź w świetle tego, czego nauczyłem się od Emila Jeřábka i po dokładniejszym przeczytaniu niektórych odpowiednich odniesień).
Jak powiedział Emil Jeřábek, krótka odpowiedź na twoje drugie pytanie brzmi: tak, ale należy zwrócić uwagę na kilka zastrzeżeń.
Przede wszystkim, to nie jest chyba oczywiste, nawet jak stwierdzają twierdzeń niezupełności Gödla w taki słaby system, nie mówiąc już udowodnić im, ponieważ zwykłe oświadczenia ilościowo nad zestawy obliczalnych aksjomatów. Zbiór aksjomatów, w przypadku których aksjomat można rozstrzygnąć jedynie za pomocą niezwykle kosztownych obliczeń, będzie trudny do wymówienia w bardzo słabym systemie. Możemy ominąć ten problem, ograniczając uwagę do „oswojonych” zbiorów aksjomatów, ponieważ obejmuje to wszystkie zbiory aksjomatów, które mają praktyczne znaczenie dla podstaw matematyki. Nawet przy tym ograniczeniu istnieje trudność techniczna z kwantyfikacją w odniesieniu do zbiorów aksjomatów, ale możemy to również ominąć, mówiąc o schemacie twierdzenia o niezupełności ; tj. dla każdego zbioru interesujących nas aksjomatów zapisujemy wzór (ograniczonej) arytmetyki w celu wyrażenia aksjomatu i mamy oddzielne wystąpienie schematu twierdzenia o niezupełności dla każdej takiej formuły.
Druga trudność polega na tym, że w przypadku bardzo słabych systemów pojawia się pytanie, czy twierdzenia o niezupełności oznaczają w ogóle to, co chcemy, aby oznaczały. Na przykład Bezboruah i Shepherdson udowodnili drugie twierdzenie Gödla o niekompletności dla Q , gdzie Q jest arytmetyką Robinsona. Ale Q jest tak słaby, że nie może nawet poprawnie sformalizować podstawowych właściwości składni, więc fakt, że Q nie dowodzi Con ( Q ), prawdopodobnie nie znaczy wiele.
Jednak po stronie dodatniej potęgowanie nie jest wymagane do arytmetyzacji składni. Na przykład w swoim Ph.D. pracy magisterskiej Bounded Arithmetic Samuel Buss przeprowadził szczegółową arytmetyzację składni za pomocą słabego systemu zwanego$S^1_2$, i udowodnił wersję drugiego twierdzenia Gödla o niezupełności dla $S^1_2$. (Rzeczywiście, własna książka Nelsona pokazuje, jak arytmetyzować podstawową składnię przy użyciu jego własnego systemu „arytmetyki predykatywnej”).
Dowód Buss wciąż nie do końca odpowiedzieć na pytanie, jakie, bo chciał wiedzieć nie tylko to, czy niekompletności twierdzenia trzymać słabych systemów; zapytałeś, czy dowody twierdzeń o niezupełności można sformalizować w systemie, który nie dowodzi, że potęgowanie jest funkcją całkowitą. Ta kwestia zdezorientowała mnie na chwilę, ponieważ dowód Bussa faktycznie odwołuje się do twierdzenia Gentzena o cięciu-eliminacji, czego nie da się udowodnić w arytmetyce ograniczonej. Jednak, jak zauważył Emil Jeřábek, dzieje się tak, ponieważ Buss udowadnia nieco mocniejszą wersję drugiego twierdzenia o niezupełności niż zwykle. Jeśli weźmiemy pod uwagę zwykłe twierdzenie o niekompletności, wówczas ekspert może „po obejrzeniu” stwierdzić, że dowód nie przekracza możliwości arytmetyki ograniczonej.
Nadal nie widziałem w literaturze wyraźnego stwierdzenia, że twierdzenia o niezupełności można udowodnić w arytmetyce ograniczonej; to wydaje się być „folklorem”. Jest wynikiem obszaru zwanego ograniczoną matematyką odwrotną . Jedną z książek, która wyraźnie realizuje program ograniczonej matematyki odwrotnej, jest Logical Foundations of Proof Complexity autorstwa Stephena Cooka i Phuong Nguyena, ale nie udowadniają one twierdzeń o niezupełności. Inną książką omawiającą twierdzenia o niekompletności dla słabych systemów jest Metamathematics of First-Order Arithmetic autorstwa Pavela Pudláka i Petra Hájka, ale nie znalazłem tam również jednoznacznego stwierdzenia.
( EDYCJA: Poprosiłem na liście mailingowej Foundations of Mathematics o publikację referencji, a Richard Heck wskazał mi: O schemacie indukcji dla ograniczonych formuł arytmetycznych autorstwa AJ Wilkie i JB Paris, Ann. Pure Appl. Logic 35 (1987), 261–302. Artykuł ten daje dość szczegółowy dowód na to, że twierdzenia o niezupełności można udowodnić na podstawie układu$I\Delta_0 + \Omega_1$ dla arytmetyki ograniczonej.)
A teraz kilka komentarzy do Twojego pierwszego pytania. Należy pamiętać, że nie zawsze łatwo było ustalić, w co wierzył Nelson, nawet gdy jeszcze żył. Nawet słaby system arytmetyki dopuszcza arbitralnie duże liczby, ale Nelson powiedział rzeczy, które wskazywały, że był podejrzliwy w stosunku do liczb, których w rzeczywistości nie można zapisać w jednoargumentowym. Kontynuując komentarz w swojej książce Predicative Arithmetic about the number$80^{5000}$, Zapytałem kiedyś Nelsona o numer$80\cdot 80 \cdots 80$ gdzie wyraźnie zapisujemy $5000$ kopie $80$. Był sceptyczny, że była to rzeczywista liczba, mimo że nie jest to potęgowanie. W takich okolicznościach nie jestem nawet pewien, czy Nelson w to wierzył$\sqrt{2}$jest irracjonalne w tym samym sensie, w jakim ty i ja w to wierzymy. Jeśli Nelson i ja mielibyśmy wspólnie przejść przez dowód, to oczywiście zgodziłby się, że każdy krok dowodu był formalnie poprawny, ale co „mówi” konkluzja dowodu? Ty i ja myślę, że mówi coś o arbitralnie dużych liczbach naturalnych, ale Nelson może tego nie robić. A jeśli nie, to dlaczego miałby w ogóle wierzyć, że poprawność krótkiej sekwencji formalnych manipulacji powinna nam coś powiedzieć (na przykład) o tym, czy komputer szuka dodatnich liczb całkowitych$a$ i $b$ takie że $a^2 = 2b^2$odniesie sukces czy porażkę? Krótko mówiąc, nie sądzę, aby próba zrozumienia dokładnie tego, w co osobiście wierzył lub wątpił Nelson, nie jest szczególnie owocna, ponieważ po prostu nie przedstawił wystarczająco szczegółowego i spójnego opisu tych przekonań.
Ciekawe omówienie „predykatywizmu” Nelsona znajduje się w artykule Interpretability in Robinson's Q , autorstwa Fernando Ferreiry i Gilda Ferreira. Co Nelson zdawał się kłócić w predykatyw arytmetyki było to, że nie należy traktować jako oświadczenie matematyczny sens o ile nie można interpretować w Q . Ferreira i Ferreira zwracają uwagę, że wykazano (Wilkie), że całości potęgowania nie można zinterpretować w Q , podczas gdy negację całości potęgowania można zinterpretować w Q (ta ostatnia jest wynikiem Solovaya). Wydaje się, że potwierdza to pogląd Nelsona, że potęgowanie stanowi „nieprzekraczalną barierę” dla zaangażowanego predykatywisty. Z drugiej strony Ferreira i Ferreira również przedstawiają argumenty, że pogląd Nelsona cierpi z powodu pewnej „niestabilności”, ponieważ na przykład nie jest zamknięty w spójności. Odsyłam czytelnika do ich artykułu w celu dokładniejszego omówienia. W każdym razie wydaje się, że warunkiem koniecznym dla Nelson zaakceptować twierdzenia niezupełności byłoby to, że są one w interpretacji Q . Wydaje mi się, że to prawda, ale znowu nie znam wyraźnego odniesienia.
Powiedziałbym, że na twoje drugie pytanie poprawnie odpowiedział Emil Jerabek. Czytając niektóre komentarze, czuję, że powinienem napisać o twoim pierwszym pytaniu:
Z rozmowy z Edem Nelsonem i ludźmi, którzy go dobrze znali, mogę powiedzieć, że Ed Nelson od dawna był mocno przekonany, że funkcja wykładnicza w jakiś sposób prowadzi do niespójności (a zatem PA jest niekonsekwentna). Pisał o tym obszernie i wskazał na pewne motywacje dla tego poglądu, jak na przykład opisanie złożoności funkcji przez Bellantoniego-Cooka i jego prace na temat predykatywności.
Wydaje się, że głębsza motywacja Eda Nelsona do jego poglądu była następująca: miał wrażenie, że w jakiś sposób konstrukcje z ustalonymi punktami (takie jak wyliczenie wszystkich częściowych funkcji rekurencyjnych lub twierdzenia Goedela o niekompletności) można `` zinternalizować '' lub sprzeczność jak „0 = 1”. Taka sprzeczność byłaby możliwa tylko przy funkcji wykładniczej. Na najbardziej podstawowym poziomie Ed Nelson nie wierzył, że pojęcie kompletnego nieskończonego zbioru jest formalnie spójne.