WikiSort.ru - Не сортированное

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

В своей формулировке теоремы о неполноте Гёдель использовал понятие ω-непротиворечивой формальной системы — более сильное условие, чем просто непротиворечивость. Формальная система называется ω-непротиворечивой, если для всякой формулы 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].

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

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

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

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

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

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

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

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

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

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

Для каждой непротиворечивой теории T можно указать такое целое значение параметра K, что уравнение

${\displaystyle {\begin{aligned}&(elg^{2}+\alpha -(b-xy)q^{2})^{2}+(q-b^{5^{60}})^{2}+(\lambda +q^{4}-1-\lambda b^{5})^{2}+\\&(\theta +2z-b^{5})^{2}+(u+t\theta -l)^{2}+(y+m\theta -e)^{2}+(n-q^{16})^{2}+\\&((g+eq^{3}+lq^{5}+(2(e-z\lambda )(1+xb^{5}+g)^{4}+\lambda b^{5}+\lambda b^{5}q^{4})q^{4})(n^{2}-n)+\\&(q^{3}-bl+l+\theta \lambda q^{3}+(b^{5}-2)q^{5})(n^{2}-1)-r)^{2}+\\&(p-2ws^{2}r^{2}n^{2})^{2}+(p^{2}k^{2}-k^{2}+1-\tau ^{2})^{2}+\\&(4(c-ksn^{2})^{2}+\eta -k^{2})^{2}+(r+1+hp-h-k)^{2}+\\&(a-(wn^{2}+1)rsn^{2})^{2}+(2r+1+\phi -c)^{2}+\\&(bw+ca-2c+4\alpha \gamma -5\gamma -d)^{2}+\\&((a^{2}-1)c^{2}+1-d^{2})^{2}+((a^{2}-1)i^{2}c^{4}+1-f^{2})^{2}+\\&(((a+f^{2}(d^{2}-a))^{2}-1)(2r+1+jc)^{2}+1-(d+of)^{2})^{2}+\\&(((z+u+y)^{2}+u)^{2}+y-K)^{2}=0\end{aligned}}}$

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

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

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

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

Каждому примитивному символу, выражению и последовательности выражений некоторой формальной системы^{[~ 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 натуральных чисел следующим образом:

n∈K ≡ ¬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], то будет иметь место ¬q∈K, то есть Bew[R(q);q] будет истинным. Следовательно, [R(q);q] вместе со своим отрицанием будет выводимо, что снова невозможно.

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

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

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

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

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