Теоремы Гёделя о неполноте

Теорема Гёделя о неполноте и вторая теорема Гёделя[~ 1] — две теоремы математической логики о принципиальных ограничениях формальной арифметики и, как следствие, всякой формальной системы, в которой можно определить основные арифметические понятия: натуральные числа, 0, 1, сложение и умножение.

Первая теорема утверждает, что если формальная арифметика непротиворечива, то в ней существует невыводимая и неопровержимая формула.

Вторая теорема утверждает, что если формальная арифметика непротиворечива, то в ней невыводима формула, содержательно утверждающая непротиворечивость этой арифметики.

Обе эти теоремы были доказаны Куртом Гёделем в 1930 году (опубликованы в 1931) и имеют непосредственное отношение ко второй проблеме из знаменитого списка Гильберта.

История

править

Ещё в начале XX века Давид Гильберт провозгласил цель аксиоматизировать всю математику, и для завершения этой задачи оставалось доказать непротиворечивость и логическую полноту арифметики натуральных чисел. 7 сентября 1930 года в Кёнигсберге проходил научный конгресс по основаниям математики, и на этом конгрессе 24-летний Курт Гёдель впервые обнародовал две фундаментальные теоремы о неполноте, показавшие, что программа Гильберта не может быть реализована: при любом выборе аксиом арифметики существуют теоремы, которые невозможно ни доказать, ни опровергнуть простыми (финитными) средствами, предусмотренными Гильбертом, а финитное доказательство непротиворечивости арифметики невозможно[6].

Это выступление не было заявлено заранее и произвело ошеломляющий эффект, Гёдель сразу стал всемирной знаменитостью, а программа Гильберта по формализации основ математики потребовала срочного пересмотра. 23 октября 1930 года результаты Гёделя были представлены Венской академии наук Хансом Ханом. Статья с обеими теоремами («О принципиально неразрешимых положениях в системе Principia Mathematica и родственных ей системах») была опубликована в научном ежемесячнике Monatshefte für Mathematik und Physik в 1931 году. Хотя доказательство второй теоремы Гёдель дал только в виде идеи, его результат был настолько ясен и неоспорим, что не вызвал сомнений ни у кого. Гильберт сразу признал ценность открытий Гёделя. Первые полные доказательства обеих теорем были опубликованы в книге Гильберта и Бернайса «Основания математики» в 1938 году. В предисловии ко второму тому авторы признали, что для достижения поставленной цели финитных методов недостаточно, и добавили в число логических средств трансфинитную индукцию. В 1936 году Герхард Генцен сумел доказать[англ.] непротиворечивость аксиом арифметики первого порядка, однако логическая полнота так и осталась недостижимой[6].

Теорема Гёделя о неполноте

править

В первоначальной форме

править

В своей формулировке теоремы о неполноте Гёдель использовал понятие ω-непротиворечивой формальной системы — более сильное условие, чем просто непротиворечивость. Формальная система называется ω-непротиворечивой, если для всякой формулы A(x) этой системы невозможно одновременно вывести формулы А(0), А(1), А(2), … и ∃x ¬A(x) (другими словами, из того, что для каждого натурального числа n выводима формула A(n), следует невыводимость формулы ∃x ¬A(x)). Легко показать, что ω-непротиворечивость влечёт простую непротиворечивость (то есть любая ω-непротиворечивая формальная система непротиворечива)[7].

В процессе доказательства теоремы строится такая формула A арифметической формальной системы S, что[7]:

Если формальная система S непротиворечива, то формула A невыводима в S; если система S ω-непротиворечива, то формула ¬A невыводима в S. Таким образом, если система S ω-непротиворечива, то она неполна[~ 2] и A служит примером неразрешимой формулы.

Формулу A иногда называют гёделевой неразрешимой формулой[8].

Интерпретация неразрешимой формулы

править

В стандартной интерпретации[~ 3] формула A означает «не существует вывода формулы A», то есть утверждает свою собственную невыводимость в S. Следовательно, по теореме Гёделя, если только система S непротиворечива, то эта формула и в самом деле невыводима в S и потому истинна в стандартной интерпретации. Таким образом, для натуральных чисел формула A верна, но в S невыводима[9].

В форме Россера

править

В процессе доказательства теоремы строится такая формула B арифметической формальной системы S, что[10]:

Если формальная система S непротиворечива, то в ней невыводимы обе формулы B и ¬B; иначе говоря, если система S непротиворечива, то она неполна[~ 2], и B служит примером неразрешимой формулы.

Формулу B иногда называют россеровой неразрешимой формулой[11]. Эта формула немного сложнее гёделевой.

Интерпретация неразрешимой формулы

править

В стандартной интерпретации[~ 3] формула B означает «если существует вывод формулы B, то существует вывод формулы ¬B». Согласно же теореме Гёделя в форме Россера, если формальная система S непротиворечива, то формула B в ней невыводима; поэтому, если система S непротиворечива, то формула B верна в стандартной интерпретации[12].

Обобщённые формулировки

править

Доказательство теоремы Гёделя обычно проводят для конкретной формальной системы (не обязательно одной и той же), соответственно утверждение теоремы оказывается доказанным только для одной этой системы. Исследование достаточных условий, которым должна удовлетворять формальная система для того, чтобы можно было провести доказательство её неполноты, приводит к обобщениям теоремы на широкий класс формальных систем. Пример обобщённой формулировки[13]:

Всякая достаточно сильная рекурсивно аксиоматизируемая непротиворечивая теория первого порядка неполна.

В частности, теорема Гёделя справедлива для каждого непротиворечивого конечно аксиоматизируемого расширения арифметической формальной системы S.

Полиномиальная форма

править

После того как Юрий Матиясевич доказал диофантовость любого эффективно перечислимого множества, и были найдены примеры универсальных диофантовых уравнений, появилась возможность сформулировать теорему о неполноте в полиномиальной (или диофантовой) форме[14][15][16][17]:

Для каждой непротиворечивой теории T можно указать такое целое значение параметра K, что уравнение
 
не имеет решений в неотрицательных целых числах, но этот факт не может быть доказан в теории T. Более того, для каждой непротиворечивой теории множество значений параметра K, обладающих таким свойством, бесконечно и алгоритмически неперечислимо.

Степень данного уравнения может быть понижена до 4 ценой увеличения количества переменных.

Набросок доказательства

править

В своей статье Гёдель даёт набросок основных идей доказательства[18], который приведён ниже с незначительными изменениями.

Каждому примитивному символу, выражению и последовательности выражений некоторой формальной системы[~ 4] S поставим в соответствие определённое натуральное число[~ 5]. Математические понятия и утверждения таким образом становятся понятиями и утверждениями о натуральных числах, и, следовательно, сами могут быть выражены в символизме системы S. Можно показать, в частности, что понятия «формула», «вывод», «выводимая формула» определимы внутри системы S, то есть можно восстановить, например, формулу F(v) в S с одной свободной натурально-числовой переменной v такую, что F(v), в интуитивной интерпретации, означает: v — выводимая формула. Теперь построим неразрешимое предложение системы S, то есть предложение A, для которого ни A, ни не-A невыводимы, следующим образом:

Формулу в S с точно одной свободной натурально-числовой переменной назовём класс-выражением. Упорядочим класс-выражения в последовательность каким-либо образом, обозначим n-е через R(n), и заметим, что понятие «класс-выражение», также как и отношение упорядочения R можно определить в системе S. Пусть α — произвольное класс-выражение; через [α;n] обозначим формулу, которая образуется из класс-выражения α заменой свободной переменной на символ натурального числа n. Тернарное отношение x = [y;z] тоже оказывается определимым в S. Теперь определим класс K натуральных чисел следующим образом:

nK ≡ ¬Bew[R(n);n] (*)

(где Bew x означает: x — выводимая формула[~ 6]). Так как все определяющие понятия из этого определения можно выразить в S, то это же верно и для понятия K, которое из них построено, то есть имеется такое класс-выражение C, что формула [C;n], интуитивно интерпретируемая, обозначает, что натуральное число n принадлежит K. Как класс-выражение, C идентично некоторому определённому R(q) в нашей нумерации, то есть

C = R(q)

выполняется для некоторого определённого натурального числа q. Теперь покажем, что предложение [R(q);q] неразрешимо в S. Так, если предложение [R(q);q] предполагается выводимым, тогда оно оказывается истинным, то есть, в соответствии со сказанным выше, q будет принадлежать K, то есть, в соответствии с (*), будет выполнено ¬Bew[R(q);q], что противоречит нашему предположению. С другой стороны, если предположить выводимым отрицание [R(q);q], то будет иметь место ¬qK, то есть Bew[R(q);q] будет истинным. Следовательно, [R(q);q] вместе со своим отрицанием будет выводимо, что снова невозможно.

Связь с парадоксами

править

В стандартной интерпретации[~ 3] гёделева неразрешимая формула A означает «не существует вывода формулы A», то есть утверждает свою собственную невыводимость в системе S. Таким образом, A является аналогом парадокса лжеца. Рассуждения Гёделя в целом очень похожи на парадокс Ришара. Более того, для доказательства существования невыводимых утверждений может быть использован любой семантический парадокс[19].

Выражаемое формулой A утверждение не содержит порочного круга, поскольку изначально утверждается только, что некоторая конкретная формула, явную запись которой получить несложно (хоть и громоздко), недоказуема. «Только впоследствии (и, так сказать, по воле случая) оказывается, что эта формула в точности та, которой выражено само это утверждение»[19].

Вторая теорема Гёделя

править

В формальной арифметике S можно построить такую формулу, которая в стандартной интерпретации[~ 3] является истинной в том и только в том случае, когда теория S непротиворечива. Для этой формулы справедливо утверждение второй теоремы Гёделя:

Если формальная арифметика S непротиворечива, то в ней невыводима формула, содержательно утверждающая непротиворечивость S.

Иными словами, непротиворечивость формальной арифметики не может быть доказана средствами этой теории. Однако, могут существовать доказательства непротиворечивости формальной арифметики, использующие средства, невыразимые в ней.

Набросок доказательства

править

Сначала строится формула Con, содержательно выражающая невозможность вывода в теории S какой-либо формулы вместе с её отрицанием. Тогда утверждение первой теоремы Гёделя выражается формулой ConG, где G — Гёделева неразрешимая формула. Все рассуждения для доказательства первой теоремы могут быть выражены и проведены средствами S, то есть в S выводима формула ConG. Отсюда, если в S выводима Con, то в ней выводима и G. Однако, согласно первой теореме Гёделя, если S непротиворечива, то G в ней невыводима. Следовательно, если S непротиворечива, то в ней невыводима и формула Con.

Историческое влияние

править

Специалисты дают самые разные, иногда даже полярные оценки исторической значимости теорем Гёделя. Часть учёных считает, что эти теоремы «перевернули» основания математики или даже всю теорию познания, и значение гениального открытия Гёделя будет постепенно открываться ещё долгое время[20]. Другие же (например, Бертран Рассел) призывают не преувеличивать, поскольку теоремы опираются на финитный формализм Гильберта[21][22].

Вопреки распространённому заблуждению, теоремы о неполноте Гёделя не предполагают, что некоторые истины так и останутся навеки непознанными. Кроме того, из этих теорем не следует, что человеческие способности к познанию так или иначе ограничены. Нет, теоремы всего лишь показывают слабости и недостатки формальных систем[23].

Рассмотрим, например, следующее доказательство непротиворечивости арифметики[24].

Допустим, что аксиоматика Пеано для арифметики противоречива. Тогда из неё можно вывести любое утверждение, в том числе ложное. Однако все аксиомы Пеано очевидным образом истинны, а из истинных утверждений не может следовать ложный вывод — получаем противоречие. Следовательно, арифметика непротиворечива.

С точки зрения повседневной человеческой логики, это доказательство приемлемо и убедительно. Но оно не может быть записано по правилам теории доказательств Гильберта, поскольку в этих правилах семантика заменена на синтаксис, а истинность — на «выводимость»[24]. В любом случае теоремы Гёделя подняли философию математики на новый уровень.

См. также

править

Примечания

править
Комментарии
  1. Иногда упоминается как вторая теорема Гёделя «о доказательствах непротиворечивости»[1], «о неполноте»[2][3][4], «о неполноте арифметики»[5].
  2. 1 2 Формальная система, содержащая неразрешимую, то есть невыводимую и неопровержимую, формулу, называется неполной.
  3. 1 2 3 4 Интерпретация формул теории S называется стандартной, если её областью является множество неотрицательных целых чисел, символ 0 интерпретируется числом 0, функциональные буквы ', +, • интерпретируются прибавлением единицы, сложением и умножением соответственно, предикатная буква = интерпретируется отношением тождества.
  4. Гёдель использовал систему Principia Mathematica Уайтхеда и Рассела с оговоркой, что рассуждения применимы к широкому классу формальных систем
  5. Подобное сопоставление формул и натуральных чисел называется арифметизацией математики и было осуществлено Гёделем впервые. Эта идея впоследствии стала ключом к решению многих важных задач математической логики. См. Гёделева нумерация
  6. «Bew» сокр. от нем. «Beweisbar» — доказуемый, выводимый
Источники
  1. Клини 1957 с.513
  2. чл.-корр. РАН Лев Дмитриевич Беклемишев в «Введении в математическую логику». Дата обращения: 7 января 2010. Архивировано 21 марта 2009 года.
  3. Толковый словарь по вычислительным системам - Page 205
  4. Доклады Академии наук СССР, Volume 262 - Page 799 (1982)
  5. Известия Академии наук СССР, Volume 50 - Page 1140 (1986)
  6. 1 2 Пиньейро, 2015, с. 13, 48—49, 66, 89—90.
  7. 1 2 Клини 1957 с.187
  8. Мендельсон 1971 с.165
  9. Это рассуждение заимствовано из Мендельсон 1971 с.160
  10. См., например, Клини 1957 с.188
  11. Мендельсон 1971 с.162
  12. Мендельсон 1971 с.162-163
  13. Мендельсон 1971 с.176
  14. Jones J. P., Undecidable diophantine equations
  15. Martin Davis, Diophantine Equations & Computation. Дата обращения: 17 ноября 2009. Архивировано из оригинала 24 мая 2010 года.
  16. Martin Davis, The Incompleteness Theorem. Дата обращения: 30 ноября 2011. Архивировано 4 марта 2016 года.
  17. К. Подниекс, Теорема Геделя в диофантовой форме. Дата обращения: 17 ноября 2009. Архивировано 10 сентября 2017 года.
  18. Gödel, Kurt. On Formally Undecidable Propositions of the Principia Mathematica and Related Systems. I. — 1931. в книге Davis, Martin (ed.). The Undecidable: Basic Papers On Undecidable Propositions, Unsolvable Problems And Computable Functions. — New York: Raven Press, 1965. — С. 6-8.
  19. 1 2 Гёдель 1931
  20. Stephen Hawking. Godel and the End of the Universe. Дата обращения: 8 апреля 2018. Архивировано из оригинала 29 мая 2020 года.
  21. Михайлова Н. В. Проблема обоснования современной математики в контексте новых философско-методологических кризисов // Философия математики: актуальные проблемы. Математика и реальность. Тезисы Третьей всероссийской научной конференции; 27-28 сентября 2013 г.. — М.: Центр стратегической конъюнктуры, 2013. — С. 187. — 270 с. — ISBN 978-5-906233-39-4. Архивировано 16 декабря 2017 года.
  22. Музыкантский А..
  23. Ливио, Марио. Был ли Бог математиком? Глава «Истина в неполноте». — М.: АСТ, 2016. — 384 с. — (Золотой фонд науки). — ISBN 978-5-17-095136-9.
  24. 1 2 Пиньейро, 2015, с. 155—162.

Литература

править

Ссылки

править

Библиография — статьи Гёделя

править
  • 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik 38: 173—198.
  • 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. and On formally undecidable propositions of Principia Mathematica and related systems I in Solomon Feferman, ed., 1986. Kurt Gödel Collected works, Vol. I. Oxford University Press: 144—195. — Оригинальный немецкий текст с параллельным английским переводом, с элементарным введением, написанным Стивеном Клини.
  • Hirzel, Martin, 2000, On formally undecidable propositions of Principia Mathematica and related systems I.. — Современный перевод Марина Херцеля.
  • 1951, Some basic theorems on the foundations of mathematics and their implications in Solomon Feferman, ed., 1995. Kurt Gödel Collected works, Vol. III. Oxford University Press: 304—323.