Курд Гёделдің «Принципиа Математика» және туыс жүйелердегі формалды шешілмейтін теоремалары

Кіріспе

1931 жылы Курт Гёдельдің "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" ("Математикалық принциптер мен байланысты жүйелердің формальды түрде шешілмейтін ұйғарымдары I") атты мақаласы – математикалық логика бойынша Курт Гёдельдің еңбегі. 1930 жылдың 17 қарашасында ұсынылған бұл мақала алғаш рет 1931 жылы Monatshefte für Mathematik und Physik журналында неміс тілінде жарияланды. Мақаланың бірнеше ағылшын тіліндегі аудармасы жарық көрді және ол классикалық математикалық логика мақалаларының екі жинағына енгізілді. Бұл мақалада Гёдельдің толық еместік теоремалары қамтылған, қазір логикадағы маңызды нәтижелер болып табылады және математикадағы дұрыстық дәлелдемелеріне зор әсер етеді. Бұл еңбек сонымен қатар Гёдельдің толық еместік теоремаларын дәлелдеу үшін жаңа әдістерді енгізгенімен де белгілі.

Негізгі нәтижелер

Негізгі нәтижелер – математикалық логика саласына зор әсер еткен Гёдельдің бірінші және екінші толық еместік теоремалары. Бұл теоремалар мақалада VI және XI теоремалар ретінде келтірілген. Бұл нәтижелерді дәлелдеу үшін Гёдель қазір Гёдель нөмірлеуі деп аталатын әдіс енгізді. Бұл әдісте әрбір сөйлем мен бірінші реттік арифметикадағы формальды дәлелге нақты бір табиғи сан тағайындалады. Гёдель осы дәлелдердің көптеген қасиеттерін бастапқы рекурсивті функцияларды анықтауға жеткілікті күшті кез келген арифметика теориясында анықтауға болатынын көрсетті. (Рекурсивті функциялар мен примитивті рекурсивті функциялар үшін қазіргі заманғы терминология қағаз жарық көрген кезде әлі қалыптаспаған еді; Гёдель қазір примитивті рекурсивті функциялар деп аталатын функциялар үшін «рекурсивті» (rekursiv) деген сөзді қолданды.) Содан бері Гёдель нөмірлеу әдісі математикалық логикада кеңінен қолданылып келеді. Гёдель нөмірлеу әдісі жаңа болғандықтан және қандай да түсініксіздіктерді болдырмау үшін, Гёдель Гёдель сандарын қолдану және тексеру үшін пайдаланылатын примитивті рекурсивті функциялар мен қатынастардың 45 нақты формальды анықтамасынан тұратын тізім ұсынды. Ол осыларды x саны φ сөйлемінің Гёдель саны болса және φ сөйлемінің дәлелінің Гёдель саны болатын табиғи сан болса ғана дұрыс болатын формуланың нақты анықтамасын беру үшін пайдаланды. Бұл формуланың атауы неміс тіліндегі «дәлел» (Beweis) сөзінен алынған. Гёдельдің осы жұмысындағы екінші жаңа әдісі – өзіне сілтеме жасайтын сөйлемдерді қолдану. Гёдель өзіне сілтеме жасайтын классикалық парадокстарды, мысалы, «Бұл мәлімдеме жалған» деген сияқты, арифметиканың өзіне сілтеме жасайтын формальды сөйлемдер ретінде қайта жазуға болатынын көрсетті. Формальды түрде, Гёдельдің бірінші толық еместік теоремасын дәлелдеу үшін қолданылатын сөйлем «Бұл мәлімдеме дәлелденбейді» дейді. Мұндай өзіне сілтеме жасау арифметика шеңберінде берілуі мүмкін екендігі Гёдельдің еңбегі жарық көргенге дейін белгілі болған жоқ; Альфред Тарскидің өзінің анықталмау теоремасы бойынша жүргізген тәуелсіз зерттеулері сол кезде жүргізілді, бірақ 1936 жылға дейін жарияланбады. 48а-шы ескертпеде Гёдель жұмыстың жоспарланған екінші бөлігінің тұрақтылық дәлелдеуі мен типтер теориясы арасындағы байланысты орнататынын (сондықтан мақала атауының соңындағы «I» бірінші бөлімді білдіреді) айтты, бірақ Гёдель қайтыс болғанға дейін жұмыстың екінші бөлігін жариялаған жоқ. Дегенмен, оның 1958 жылғы «Диалектика» журналындағы мақаласы типтер теориясының арифметиканың тұрақтылығын дәлелдеу үшін қалай қолданылатынын көрсетті.

The main results established are Gödel's first and second incompleteness theorems, which have had an enormous impact on the field of mathematical logic. These appear as theorems VI and XI, respectively, in the paper. In order to prove these results, Gödel introduced a method now known as Gödel numbering. In this method, each sentence and formal proof in first order arithmetic is assigned a particular natural number. Gödel shows that many properties of these proofs can be defined within any theory of arithmetic that is strong enough to define the primitive recursive functions. (The contemporary terminology for recursive functions and primitive recursive functions had not yet been established when the paper was published; Gödel used the word rekursiv ("recursive") for what are now known as primitive recursive functions.) The method of Gödel numbering has since become common in mathematical logic. Because the method of Gödel numbering was novel, and to avoid any ambiguity, Gödel presented a list of 45 explicit formal definitions of primitive recursive functions and relations used to manipulate and test Gödel numbers. He used these to give an explicit definition of a formula that is true if and only if x is the Gödel number of a sentence φ and there exists a natural number that is the Gödel number of a proof of φ. The name of this formula derives from Beweis, the German word for proof. A second new technique invented by Gödel in this paper was the use of self referential sentences. Gödel showed that the classical paradoxes of self reference, such as "This statement is false", can be recast as self referential formal sentences of arithmetic. Informally,
the sentence employed to prove Gödel's first incompleteness theorem says "This statement is not provable." The fact that such self reference can be expressed within arithmetic was not known until Gödel's paper appeared; independent work of Alfred Tarski on his indefinability theorem was conducted around the same time but not published until 1936. In footnote 48a, Gödel stated that a planned second part of the paper would establish a link between consistency proofs and type theory (hence the "I" at the end of the paper's title, denoting the first part), but Gödel did not publish a second part of the paper before his death. His 1958 paper in Dialectica did, however, show how type theory can be used to give a consistency proof for arithmetic.

Ағылшын тілінен аударылған басылымдар

Оның өмірінде Гёдельдің еңбегінің үш ағылшын тіліндегі аудармасы жарық көрді, бірақ бұл процесс қиындықтарсыз болған жоқ. Бірінші ағылшын аудармасын Бернард Мелтцер жасаған; ол 1963 жылы Basic Books баспасында жеке кітап ретінде басылып шықты, кейіннен Dover және Хокинг баспаларында қайта басылды (God Created the Integers, Running Press, 2005:1097ff). Мелтцердің нұсқасын Раймонд Смуллиан «жақсы аударма» деп сипаттаған, бірақ оны Стефан Бауэр Менгельберг (1966) жағымсыз бағалады. Доусонның Гёдельдің өмірбаянында айтылғандай (Dawson 1997:216),
Бақытымызға орай, Мелтцердің аудармасы көп ұзамай Эллиотт Мендельсон жасаған, Мартин Дэвистің «The Undecidable» антологиясы үшін дайындалған жақсырақ аудармамен алмастырылды; алайда, бұл да соңғы сәттерге дейін Гёдельдің назарына жеткізілмеді, және жаңа аударма да оның толық пікіріне сай келмеді. Басқа мәтінді қарастыруға уақыт жоқ екенін естігенде, ол Мендельсонның аудармасын «жалпы алғанда өте жақсы» деп мойындады және оны жариялауға келісті. [Бірақ кейін ол келісіміне өкінді, себебі басылып шыққан том нашар типография және көптеген қателіктермен бұзылған еді.] Эллиотт Мендельсонның аудармасы «The Undecidable» жинағында қол жетімді (Davis 1965:5ff). Бұл аударманы Бауэр Менгельберг (1966) де қатаң сынға алды, ол баспа қателіктерінің толық тізімін бергеннен басқа, аудармадағы маңызды қателер деп санайтын нәрселерді де сипаттады. Жан ван Хейеноорттың аудармасы «Фрегеден Гёделге дейін: Математикалық логиканың дереккөздер кітабы» жинағында (van Heijenoort 1967) жарияланған. Алонзо Черч (1972) оны «қазірге дейін жасалған ең мұқият аударма» деп атады, бірақ оған да бірнеше сын ескертпелер жасады. Доусон (1997:216) мынадай мәлімдейді:
Гёдель ең көп бағалаған аударма Жан ван Хейеноорттың аудармасы болды. Ван Хейеноорт томның алғы сөзінде Гёдельдің өзінің еңбектерінің аудармаларын жеке оқып, бекіткен төрт автордың бірі екенін атап өтті. Бұл бекіту процесі еңбек талап етті. Гёдель 1931 жылғы мәтініне өзгерістер енгізді, ал ер адамдар арасындағы келіссөздер «ұзаққа созылды»: «Жеке ван Хейеноорт Гёдельді ол білген ең талапкер адам деп мәлімдеді». Олар «жеті жүздей хат алмасып, неміс және ағылшын тіліндегі сөздердің мағынасы мен қолданысына қатысты мәселелерді шешу үшін Гёдельдің кеңсесінде екі рет кездесті» (Dawson 1997:216 217). Түпнұсқалық мақаланың тікелей аудармасы болмаса да, «Годельдің 1931 жылғы шешілмейтін туралы түпнұсқалық мақаласында қамтылғанға ұқсас мәселелерді қамтитын» (Davis 1952:39) өте пайдалы 4-ші нұсқа бар, сондай-ақ Гёдельдің тақырыпқа қатысты өз кеңейтулері мен түсініктемелері де бар. Бұл «Формальды математикалық жүйелердің шешілмейтін ұйғарымдары туралы» (Davis 1965:39ff) деп аталады және 1934 жылы Нью-Джерси штатының Принстон қаласындағы Жоғары оқу институтында Гёдель оқыған лекцияларының Стивен Клин және Дж. Баркли Россер жасаған стенограммасы болып табылады. Дэвис осы нұсқаға Гёдельдің екі беттік қателіктері мен қосымша түзетулерін қосты. Бұл нұсқа да маңызды, себебі онда Гёдель алғаш рет рекурсияның (жалпы, яғни Гербранд-Гёдель) түрін тудырған Гербрандтың ұсынысын сипаттайды.

During his lifetime three English translations of Gödel's paper were printed, but the process was not without difficulty. The first English translation was by Bernard Meltzer; it was published in 1963 as a standalone work by Basic Books and has since been reprinted by Dover and reprinted by Hawking (God Created the Integers, Running Press, 2005:1097ff). The Meltzer version—described by Raymond Smullyan as a 'nice translation'—was adversely reviewed by Stefan Bauer Mengelberg (1966). According to Dawson's biography of Gödel (Dawson 1997:216),
Fortunately, the Meltzer translation was soon supplanted by a better one prepared by Elliott Mendelson for Martin Davis's anthology The Undecidable; but it too was not brought to Gödel's attention until almost the last minute, and the new translation was still not wholly to his liking when informed that there was not time enough to consider substituting another text, he declared that Mendelson's translation was 'on the whole very good' and agreed to its publication. [Afterward he would regret his compliance, for the published volume was marred throughout by sloppy typography and numerous misprints.] The translation by Elliott Mendelson appears in the collection The Undecidable (Davis 1965:5ff). This translation also received a harsh review by Bauer Mengelberg (1966), who in addition to giving a detailed list of the typographical errors also described what he believed to be serious errors in the translation. A translation by Jean van Heijenoort appears in the collection From Frege to Gödel: A Source Book in Mathematical Logic (van Heijenoort 1967). A review by Alonzo Church (1972) described this as "the most careful translation that has been made" but also gave some specific criticisms of it. Dawson (1997:216) notes:
The translation Gödel favored was that by Jean van Heijenoort In the preface to the volume van Heijenoort noted that Gödel was one of four authors who had personally read and approved the translations of his works. This approval process was laborious. Gödel introduced changes to his text of 1931, and negotiations between the men were "protracted": "Privately van Heijenoort declared that Gödel was the most doggedly fastidious individual he had ever known." Between them they "exchanged a total of seventy letters and met twice in Gödel's office in order to resolve questions concerning subtleties in the meanings and usage of German and English words." (Dawson 1997:216 217). Although not a translation of the original paper, a very useful 4th version exists that "cover[s] ground quite similar to that covered by Godel's original 1931 paper on undecidability" (Davis 1952:39), as well as Gödel's own extensions of and commentary on the topic. This appears as On Undecidable Propositions of Formal Mathematical Systems (Davis 1965:39ff) and represents the lectures as transcribed by Stephen Kleene and J. Barkley Rosser while Gödel delivered them at the Institute for Advanced Study in Princeton, New Jersey in 1934. Two pages of errata and additional corrections by Gödel were added by Davis to this version. This version is also notable because in it Gödel first describes the Herbrand suggestion that gave rise to the (general, i. e. Herbrand–Gödel) form of recursion.