Virtual Laboratory Wiki
Advertisement
Kurt gödel 1925

Курт Гёдель (нем. Kurt Friedrich Gödel)

Курт Фри́дрих Гёдель (нем. Kurt Friedrich Gödel; 19061978) — австрийский логик, математик и философ математики, наиболее известный сформулированной и доказанной им теоремой о неполноте.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Каждому примитивному символу, выражению и последовательности выражений некоторой формальной системы[~ 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 является аналогом парадокса лжеца. Рассуждения Гёделя в целом очень похожи на парадокс Ришара. Более того, для доказательства существования невыводимых утверждений может быть использован любой семантический парадокс[17].

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

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

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

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

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

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

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

Исторические сведения[]

23 октября 1930 года результаты Гёделя были представлены Венской академии наук Хансом Ханом. Основная статья была получена для публикации 17 ноября 1930 года и опубликована в начале 1931 года[18].

Пределы применимости теоремы Гёделя о неполноте[]

Рядовой российский врач, мультидисциплинарный исследователь и зобретатель, член Московского общества испытателей природы Макеев А.К. показал ограниченность применения теоремы Гёделя о неполноте только в пределах специализированных теорий и неприменимость в отношении всеобъемлющего эволюционирующего естественнонаучного всезнания: Опровержение теоремы Гёделя о неполноте.

Примечания[]

  1. Иногда упоминается как вторая теорема Гёделя «о доказательствах непротиворечивости»[1], «о неполноте»[2][3][4], «о неполноте арифметики»[5].
  2. 2,0 2,1 Формальная система, содержащая неразрешимую, то есть невыводимую и неопровержимую, формулу, называется неполной.
  3. 3,0 3,1 3,2 3,3 Интерпретация формул теории S называется стандартной, если её областью является множество неотрицательных целых чисел, символ 0 интерпретируется числом 0, функциональные буквы ', +, • интерпретируются прибавлением единицы, сложением и умножением соответственно, предикатная буква = интерпретируется отношением тождества.
  4. Гёдель использовал систему Principia Mathematica Уайтхеда и Рассела с оговоркой, что рассуждения применимы к широкому классу формальных систем
  5. Подобное сопоставление формул и натуральных чисел называется арифметизацией математики и было осуществлено Гёделем впервые. Эта идея впоследствии стала ключом к решению многих важных задач математической логики. См. Гёделева нумерация
  6. "Bew" сокр. от нем. "Beweisbar" - доказуемый, выводимый

Источники[]

  1. Клини 1957 с.513
  2. чл.-корр. РАН Лев Дмитриевич Беклемишев в «Введении в математическую логику»
  3. Толковый словарь по вычислительным системам‎ - Page 205
  4. Доклады Академии наук СССР, Volume 262‎ - Page 799 (1982)
  5. Известия Академии наук СССР, Volume 50‎ - Page 1140 (1986)
  6. 6,0 6,1 Клини 1957 с.187
  7. Мендельсон 1971 с.165
  8. Это рассуждение заимствовано из Мендельсон 1971 с.160
  9. См., например, Клини 1957 с.188
  10. Мендельсон 1971 с.162
  11. Мендельсон 1971 с.162-163
  12. Мендельсон 1971 с.176
  13. Jones J. P., Undecidable diophantine equations
  14. Martin Davis, Diophantine Equations & Computation
  15. К. Подниекс, Теорема Геделя в диофантовой форме
  16. 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.
  17. 17,0 17,1 Гёдель 1931
  18. Heijenoort 1967 p.592

Литература[]

  • Davis, Martin (ed.) The Undecidable: Basic Papers On Undecidable Propositions, Unsolvable Problems And Computable Functions. — New York: Raven Press, 1965. — 440 p.
  • Heijenoort, Jean van (ed.) From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. — Cambridge, Massachusetts: Harvard University Press, 1967. — 660 p.

См. также[]

Advertisement