" Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I " (" О формально неразрешимых предложениях Principia Mathematica и связанных с ними систем I ") — статья по математической логике Курта Гёделя . Представленная 17 ноября 1930 года, она была первоначально опубликована на немецком языке в выпуске Monatshefte für Mathematik und Physik за 1931 год . Несколько английских переводов появились в печати, и статья была включена в два сборника классических статей по математической логике. Статья содержит теоремы Гёделя о неполноте , которые теперь являются фундаментальными результатами в логике, имеющими множество последствий для доказательств непротиворечивости в математике. Статья также известна введением новых методов, которые Гёдель изобрёл для доказательства теорем о неполноте.
Основными установленными результатами являются первая и вторая теоремы Гёделя о неполноте , которые оказали огромное влияние на область математической логики . Они появляются в статье как теоремы VI и XI соответственно.
Для доказательства этих результатов Гёдель ввел метод, который теперь известен как нумерация Гёделя . В этом методе каждому предложению и формальному доказательству в арифметике первого порядка присваивается определенное натуральное число. Гёдель показывает, что многие свойства этих доказательств могут быть определены в рамках любой теории арифметики, которая достаточно сильна, чтобы определить примитивно-рекурсивные функции . (Современная терминология для рекурсивных функций и примитивно-рекурсивных функций еще не была установлена, когда статья была опубликована; Гёдель использовал слово rekursiv («рекурсивный») для того, что теперь известно как примитивно-рекурсивные функции.) Метод нумерации Гёделя с тех пор стал общепринятым в математической логике.
Поскольку метод нумерации Гёделя был новым, и чтобы избежать какой-либо двусмысленности, Гёдель представил список из 45 явных формальных определений примитивных рекурсивных функций и отношений, используемых для манипулирования и проверки чисел Гёделя. Он использовал их, чтобы дать явное определение формулы Bew( x ) , которая истинна тогда и только тогда, когда x является номером Гёделя предложения φ и существует натуральное число, которое является номером Гёделя доказательства φ . Название этой формулы происходит от Beweis , немецкого слова, обозначающего доказательство.
Вторым новым приемом, изобретенным Гёделем в этой статье, было использование самореферентных предложений. Гёдель показал, что классические парадоксы самореферентности, такие как « Это утверждение ложно », могут быть переделаны в самореферентные формальные предложения арифметики. Неформально, предложение, использованное для доказательства первой теоремы Гёделя о неполноте, гласит: «Это утверждение недоказуемо». Тот факт, что такая самореферентность может быть выражена в арифметике, не был известен до появления статьи Гёделя; независимая работа Альфреда Тарского по его теореме о неопределенности была проведена примерно в то же время, но не была опубликована до 1936 года.
В сноске 48a Гёдель заявил, что запланированная вторая часть статьи установит связь между доказательствами непротиворечивости и теорией типов (отсюда «I» в конце названия статьи, обозначающее первую часть), но Гёдель не опубликовал вторую часть статьи до своей смерти. Однако его статья 1958 года в Dialectica показала, как теория типов может быть использована для доказательства непротиворечивости арифметики.
При его жизни было напечатано три английских перевода статьи Гёделя, но процесс не был без трудностей. Первый английский перевод был сделан Бернардом Мельцером ; он был опубликован в 1963 году как отдельная работа Basic Books и с тех пор был переиздан Dover и переиздан Хокингом ( God Created the Integers , Running Press, 2005:1097ff). Версия Мельцера, описанная Рэймондом Смаллианом как «хороший перевод», была негативно оценена Стефаном Бауэром-Менгельбергом (1966). Согласно биографии Гёделя, написанной Доусоном (Dawson 1997:216),
К счастью, перевод Мельцера вскоре был заменен лучшим переводом, подготовленным Эллиотом Мендельсоном для антологии Мартина Дэвиса «Неразрешимое» ; но и он не был представлен вниманию Гёделя до последней минуты, и новый перевод все еще не полностью ему нравился... когда ему сообщили, что нет времени рассмотреть возможность замены другим текстом, он заявил, что перевод Мендельсона «в целом очень хорош», и согласился на его публикацию. [Впоследствии он пожалел о своей уступке, поскольку опубликованный том был испорчен неряшливой типографикой и многочисленными опечатками.]
Перевод Эллиота Мендельсона появляется в сборнике The Undecidable (Davis 1965:5ff). Этот перевод также получил резкую рецензию от Бауэра-Менгельберга (1966), который в дополнение к подробному списку типографских ошибок также описал то, что он считал серьезными ошибками в переводе.
Перевод Жана ван Хейеноорта представлен в сборнике From Frege to Gödel: A Source Book in Mathematical Logic (van Heijenoort 1967). В обзоре Алонзо Чёрча (1972) этот перевод описывается как «самый тщательный перевод, который был сделан», но также даются некоторые конкретные критические замечания. Доусон (1997:216) отмечает:
Перевод, которому отдал предпочтение Гёдель, был сделан Жаном ван Хейеноортом... В предисловии к тому ван Хейеноорт отметил, что Гёдель был одним из четырех авторов, которые лично прочитали и одобрили переводы его работ.
Этот процесс утверждения был трудоемким. Гёдель внес изменения в свой текст 1931 года, и переговоры между мужчинами были «затяжными»: «В частном порядке ван Хейеноорт заявил, что Гёдель был самым упрямым и скрупулезным человеком, которого он когда-либо знал». Между собой они «обменялись в общей сложности семьюдесятью письмами и дважды встречались в офисе Гёделя, чтобы разрешить вопросы, касающиеся тонкостей в значениях и использовании немецких и английских слов» (Dawson 1997:216-217).
Хотя это и не перевод оригинальной статьи, существует очень полезная 4-я версия, которая «охватывает тему, весьма похожую на ту, что была охвачена оригинальной статьей Гёделя 1931 года о неразрешимости» (Davis 1952:39), а также собственные расширения и комментарии Гёделя по этой теме. Она появляется как « О неразрешимых предложениях формальных математических систем» (Davis 1965:39ff) и представляет собой лекции, расшифрованные Стивеном Клини и Дж. Баркли Россером, когда Гёдель читал их в Институте перспективных исследований в Принстоне, штат Нью-Джерси, в 1934 году. Две страницы опечаток и дополнительных исправлений Гёделя были добавлены Дэвисом к этой версии. Эта версия также примечательна тем, что в ней Гёдель впервые описывает предположение Эрбрана , которое привело к (общей, т. е. Эрбранда–Гёделя) форме рекурсии .