O formalnie nierozstrzygalnych propozycjach Principia Mathematica i systemów pokrewnych - On Formally Undecidable Propositions of Principia Mathematica and Related Systems

Ten artykuł dotyczy papieru. Dla twierdzeń udowodnionych w tym artykule, zobacz twierdzenia Gödla o niezupełności .

„ Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I ” („ O formalnie nierozstrzygalnych twierdzeniach Principia Mathematica i systemów pokrewnych I ”) to artykuł z logiki matematycznej autorstwa Kurta Gödla . Przesłany 17 listopada 1930 r. został pierwotnie opublikowany w języku niemieckim w tomie Monatshefte für Mathematik z 1931 r . W druku ukazało się kilka przekładów na język angielski, a artykuł został włączony do dwóch zbiorów klasycznych artykułów z zakresu logiki matematycznej. Artykuł zawiera twierdzenia Gödla o niezupełności , obecnie fundamentalne wyniki w logice, które mają wiele implikacji dla dowodów zgodności w matematyce. Artykuł znany jest również z wprowadzenia nowych technik, które wymyślił Gödel, aby udowodnić twierdzenia o niezupełności.

Zarys i kluczowe wyniki

Główne uzyskane wyniki to pierwsze i drugie twierdzenie o niezupełności Gödla , które wywarły ogromny wpływ na dziedzinę logiki matematycznej . Pojawiają się one w artykule jako twierdzenia odpowiednio VI i XI.

Aby udowodnić te wyniki, Gödel wprowadził metodę znaną obecnie jako numeracja Gödla . W tej metodzie każdemu zdaniu i dowodowi formalnemu w arytmetyce pierwszego rzędu przypisywana jest konkretna liczba naturalna. Gödel pokazuje, że wiele właściwości tych dowodów można zdefiniować w ramach dowolnej teorii arytmetyki, która jest wystarczająco silna, aby zdefiniować prymitywne funkcje rekurencyjne . (Współczesna terminologia dla funkcji rekurencyjnych i pierwotnych funkcji rekurencyjnych nie została jeszcze ustalona, ​​kiedy artykuł został opublikowany; Gödel używał słowa rekursiv ("rekurencyjne") dla tego, co obecnie znane jest jako pierwotne funkcje rekurencyjne.) Metoda numeracji Gödla jest od tego czasu stają się powszechne w logice matematycznej.

Ponieważ metoda numerowania Gödla była nowa i aby uniknąć wszelkich niejasności, Gödel przedstawił listę 45 wyraźnych formalnych definicji pierwotnych funkcji i relacji rekurencyjnych używanych do manipulowania i testowania liczb Gödla. Użył ich do podania wyraźnej definicji formuły Bew( x ), która jest prawdziwa wtedy i tylko wtedy, gdy x jest liczbą Gödla zdania φ i istnieje liczba naturalna, która jest liczbą Gödla dowodu φ. Nazwa tej formuły wywodzi się od Beweis , niemieckiego słowa oznaczającego dowód.

Drugą nową techniką wymyśloną przez Gödla w tym artykule było użycie zdań autoodniesienia. Gödel wykazał, że klasyczne paradoksy samoodniesienia , takie jak „ To stwierdzenie jest fałszywe ”, można przekształcić w samoodnoszące się formalne zdania arytmetyczne. Nieformalnie zdanie użyte do udowodnienia pierwszego twierdzenia Gödla o niezupełności mówi: „To stwierdzenie nie jest udowodnione”. Fakt, że takie odniesienie do siebie można wyrazić w arytmetyce, nie był znany do czasu pojawienia się artykułu Gödla; samodzielna praca Alfreda Tarskiego nad jego twierdzeniem o niedefiniowalności została przeprowadzona w tym samym czasie, ale opublikowana dopiero w 1936 roku.

W przypisie 48a Gödel stwierdził, że planowana druga część artykułu ustaliłaby powiązanie między dowodami spójności a teorią typów, ale Gödel nie opublikował drugiej części artykułu przed śmiercią. Jego artykuł w Dialectica z 1958 roku pokazał jednak, w jaki sposób teoria typów może być wykorzystana do uzyskania dowodu spójności arytmetyki.

Opublikowane tłumaczenia na język angielski

Za jego życia wydrukowano trzy angielskie tłumaczenia papieru Gödla, ale proces ten nie przebiegał bez trudności. Pierwszym angielskim tłumaczeniem był Bernard Meltzer; została opublikowana w 1963 jako samodzielna praca przez Basic Books i od tego czasu została przedrukowana przez Dover i przedrukowana przez Hawkinga ( God Created the Integers , Running Press, 2005:1097ff). Wersja Meltzera – opisana przez Raymonda Smullyana jako „ładne tłumaczenie” – została negatywnie zrecenzowana przez Stefana Bauera-Mengelberga (1966). Według biografii Gödla Dawsona (Dawson 1997:216),

Na szczęście tłumaczenie Meltzera zostało wkrótce zastąpione lepszym, przygotowanym przez Elliotta Mendelsona do antologii Martina Davisa The Undecidable ; ale też nie zwrócił na to uwagi Gödla aż do ostatniej chwili, a nowe tłumaczenie wciąż nie w pełni mu się podobało… kiedy poinformowano go, że nie ma wystarczająco dużo czasu, aby rozważyć zastąpienie innym tekstem, oświadczył, że tłumaczenie Mendelsona było „ ogólnie bardzo dobrze” i wyraził zgodę na jego publikację. 3 [ 3 Potem żałował, że się podporządkował, gdyż opublikowany tom był splamiony niechlujną typografią i licznymi błędami drukarskimi.]

Tłumaczenie Elliotta Mendelsona pojawia się w zbiorze Nierozstrzygalni (Davis 1965:5ff). Przekład ten otrzymał również surową recenzję Bauera-Mengelberga (1966), który oprócz szczegółowej listy błędów typograficznych opisał również to, co uważał za poważne błędy w tłumaczeniu.

Tłumaczenie Jeana van Heijenoorta pojawia się w zbiorze From Frege to Gödel: A Source Book in Mathematical Logic (van Heijenoort 1967). Recenzja Alonzo Churcha (1972) określiła to jako „najstaranniejsze tłumaczenie, jakie zostało wykonane”, ale także przedstawiła kilka konkretnych uwag krytycznych. Dawson (1997:216) zauważa:

Preferowanym przez Gödla przekładem był Jean van Heijenoort... We wstępie do tomu van Heijenoort zauważył, że Gödel był jednym z czterech autorów, którzy osobiście czytali i zatwierdzali przekłady jego dzieł.

Ten proces zatwierdzania był pracochłonny. Gödel wprowadził zmiany do swojego tekstu z 1931 roku, a negocjacje między mężczyznami „przeciągały się”: „Prywatnie van Heijenoort oświadczył, że Gödel był najbardziej wybredną osobą, jaką kiedykolwiek znał”. Pomiędzy nimi „wymienili w sumie siedemdziesiąt listów i spotkali się dwukrotnie w biurze Gödla w celu rozwiązania kwestii dotyczących subtelności w znaczeniach i użyciu słów niemieckich i angielskich”. (Dawson 1997:216-217).

Chociaż nie jest to tłumaczenie oryginalnego artykułu, istnieje bardzo użyteczna czwarta wersja, która „obejmuje grunty całkiem podobne do tego, o którym mowa w oryginalnym artykule Gödla z 1931 roku na temat nierozstrzygalności” (Davis 1952:39), jak również własne rozszerzenia i komentarz na ten temat. Pojawia się on jako On Undecidable Propositions of Formal Mathematical Systems (Davis 1965:39ff) i przedstawia wykłady przepisane przez Stephena Kleene i J. Barkley Rossera, podczas gdy Gödel wygłosił je w Institute for Advanced Study w Princeton NJ w 1934 roku. Dwie strony erraty a dodatkowe poprawki Gödla zostały dodane przez Davisa do tej wersji. Ta wersja jest również godna uwagi, ponieważ Gödel po raz pierwszy opisuje w niej sugestię Herbranda, która dała początek (ogólnej, tj. Herbrand-Gödel) formie rekurencji .

Zobacz też

Bibliografia

  • Stefan Bauer-Mengelberg (1966). Przegląd The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions. The Journal of Symbolic Logic , tom. 31, nr 3. (wrzesień 1966), s. 484–494.
  • Kościół Alonza (1972). Przegląd książki źródłowej w logice matematycznej 1879-1931. The Journal of Symbolic Logic , tom. 37, nr 2. (czerwiec 1972), s. 405.
  • Martin Davis , wyd. (1965). The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions , Raven, New York. Przedruk, Dover, 2004. ISBN  0-486-43228-9 .
  • Martina Davisa , (2000). Silniki logiki: matematyka i pochodzenie komputera , W. w. Norton & Company, Nowy Jork. ISBN  0-393-32229-7 pbk.
  • Kurt Gödel (1931), „Über formalne unentscheidbare Sätze der Principia Mathematica und Verwandter Systeme, I.” Monatshefte für Mathematik und Physik 38 : 173-198. DOI 10.1007/BF01700692 Dostępne online przez SpringerLink.
  • Kurta Gödla (1958). „Über eine bisher noch nicht benüzte Erweiterung des finiten Standpunktes”. Dialectica, t . 12, s. 280–287. Przedrukowano w tłumaczeniu na język angielski w Dziełach zebranych Gödla , t. II, Soloman Feferman i in., wyd. Oxford University Press, 1990.
  • Jean van Heijenoort , wyd. (1967). Od Fregego do Gödla: książka źródłowa o logice matematycznej 1879-1931 . Wydawnictwo Uniwersytetu Harvarda.
  • Bernarda Meltzera (1962). O nierozstrzygalnych formalnie twierdzeniach Principia Mathematica i systemów pokrewnych. Tłumaczenie niemieckiego oryginału Kurta Gödela, 1931. Basic Books, 1962. Przedruk, Dover, 1992. ISBN  0-486-66980-7 .
  • Raymond Smullyan (1966). Przegląd „ Forally Undecidable Propositions of Principia Mathematica and Related Systems”. Amerykański miesięcznik matematyczny , tom. 73, nr 3. (marzec 1966), s. 319–322.
  • Johna W. Dawsona , (1997). Dylematy logiczne: życie i twórczość Kurta Gödla , AK Peters, Wellesley, MA. ISBN  1-56881-256-6 .

Linki zewnętrzne