О статье Гёделя «О формально неразрешимых предложениях Principia Mathematica»

Введение

Статья Курта Гёделя 1931 года "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" ("О формально неразрешимых предложениях Principia Mathematica и связанных систем I") является работой по математической логике, написанной Куртом Гёделем. Поданная в редакцию 17 ноября 1930 года, она была впервые опубликована на немецком языке в 1931 году в томе журнала Monatshefte für Mathematik und Physik. Существует несколько английских переводов этой статьи, и она была включена в две сборники классических работ по математической логике. В статье содержатся теоремы о неполноте Гёделя – фундаментальные результаты логики, имеющие множество следствий для доказательств непротиворечивости в математике. Статья также известна тем, что в ней представлены новые методы, разработанные Гёделем для доказательства теорем о неполноте.

Конспекты и основные результаты

Основными установленными результатами являются первая и вторая теоремы о неполноте Гёделя, оказавшие огромное влияние на область математической логики. В статье они представлены как теоремы VI и XI соответственно. Для доказательства этих результатов Гёдель ввёл метод, известный как нумерация Гёделя. В этом методе каждому предложению и формальному доказательству в арифметике первого порядка присваивается определённое натуральное число. Гёдель показал, что многие свойства этих доказательств могут быть определены в любой теории арифметики, достаточно сильной для определения примитивных рекурсивных функций. (Современная терминология для рекурсивных и примитивных рекурсивных функций ещё не была установлена к моменту публикации статьи; Гёдель использовал слово *rekursiv* ("рекурсивный") для обозначения того, что сейчас известно как примитивные рекурсивные функции.) Метод нумерации Гёделя с тех пор стал общепринятым в математической логике. Поскольку метод нумерации Гёделя был новым, и чтобы избежать какой-либо двусмысленности, Гёдель представил список из 45 явных формальных определений примитивных рекурсивных функций и отношений, используемых для манипулирования и проверки чисел Гёделя. Он использовал их для дания явного определения формулы, которая истинна тогда и только тогда, когда *x* является числом Гёделя предложения φ и существует натуральное число, являющееся числом Гёделя доказательства φ. Название этой формулы происходит от немецкого слова *Beweis*, означающего доказательство. Вторая новая техника, изобретённая Гёделем в этой статье, заключалась в использовании самореферентных предложений. Гёдель показал, что классические парадоксы самоссылки, такие как «Это утверждение ложно», могут быть переформулированы как самореферентные формальные предложения арифметики. Неформально, предложение, используемое для доказательства первой теоремы о неполноте Гёделя, гласит: «Это утверждение не доказуемо». Тот факт, что такая самоссылка может быть выражена средствами арифметики, был неизвестен до появления работы Гёделя; независимая работа Альфреда Тарского над его теоремой об определимости проводилась примерно в то же время, но была опубликована только в 1936 году. В примечании 48a Гёдель указал, что запланированная вторая часть работы установит связь между доказательствами непротиворечивости и теорией типов (отсюда и «I» в конце названия статьи, обозначающая первую часть), но Гёдель не опубликовал вторую часть работы при жизни. Его статья 1958 года в журнале *Dialectica* показала, как теорию типов можно использовать для доказательства непротиворечивости арифметики.

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), к счастью, перевод Мельцера вскоре был заменен более качественным переводом, подготовленным Эллиотом Мендельсоном для антологии Мартина Дэвиса «Неразрешимые предложения»; однако Гёдель узнал о нем почти в последнюю минуту, и новый перевод не вполне его устраивал. Когда ему сообщили, что времени на рассмотрение другого варианта уже нет, он заявил, что перевод Мендельсона «в целом очень хорош» и согласился на его публикацию. [Позже он пожалел об этом, поскольку опубликованный том был испорчен небрежной версткой и многочисленными опечатками.] Перевод Эллиота Мендельсона опубликован в сборнике «Неразрешимые предложения» (Davis 1965:5ff). Этот перевод также получил резкую рецензию Бауэра Менгельберга (1966), который, помимо подробного списка типографских ошибок, указал на, по его мнению, серьезные ошибки в переводе. Перевод Жана ван Хейеноорта опубликован в сборнике «От Фреге до Гёделя: Источниковая книга по математической логике» (van Heijenoort 1967). В рецензии Алонзо Черча (1972) он был назван «наиболее тщательным из всех выполненных переводов», но также подвергся некоторой критике. Доусон (1997:216) отмечает: Перевод, который предпочитал Гёдель, был выполнен Жаном ван Хейеноортом. В предисловии к этому тому ван Хейеноорт отметил, что Гёдель был одним из четырех авторов, лично прочитавших и одобривших переводы своих работ. Этот процесс одобрения был трудоемким. Гёдель вносил изменения в свой текст 1931 года, и переговоры между ними были «долгими»: «В частной беседе ван Хейеноорт заявил, что Гёдель был самым педантичным и требовательным человеком, которого он когда-либо встречал». Они «обменялись в общей сложности семьюдесятью письмами и дважды встречались в кабинете Гёделя, чтобы разрешить вопросы, касающиеся тонкостей в значениях и употреблении немецких и английских слов» (Dawson 1997:216–217). Хотя это и не перевод оригинальной статьи, существует очень полезная четвертая версия, которая «охватывает материал, во многом схожий с тем, что представлен в оригинальной статье Гёделя 1931 года о неразрешимости» (Davis 1952:39), а также собственные расширения и комментарии Гёделя к этой теме. Она опубликована под названием «О неопределенных предложениях формальных математических систем» (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.