Введение

Доказательство теоремы о полноте Гёделя, представленное Куртом Гёделем в его докторской диссертации 1929 года (и более краткая версия доказательства, опубликованная в 1930 году в виде статьи под названием «О полноте аксиом функционального исчисления высказываний» (на немецком языке)), трудно воспринимается сегодня; в нём используются понятия и формализмы, которые устарели, а также терминология, которая часто неясна. Приведённое ниже изложение стремится точно воспроизвести все шаги доказательства и все ключевые идеи, переформулировав его на современном языке математической логики. Следует понимать, что данный обзор не является строгим доказательством теоремы.

Предположения

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

Заявление теоремы и ее доказательство

В дальнейшем мы приведем две эквивалентные формулировки теоремы и докажем их эквивалентность. Доказательство теоремы будет проведено следующими шагами:

Сведение теоремы к предложениям (формулам без свободных переменных) в пренексной форме, то есть с размещением всех кванторов (∀ и ∃) в начале. Кроме того, мы приведем ее к формулам, первый квантор которых – ∀. Это возможно, поскольку для любого предложения существует эквивалентное предложение в пренексной форме, первый квантор которого – ∀. Сведем теорему к предложениям вида ∀x₁ ∀x₂ … ∀xₖ ∃y₁ ∃y₂ … ∃yₘ φ(x₁ … xₖ, y₁ … yₘ). Хотя мы не можем добиться этого простым переупорядочиванием кванторов, мы покажем, что достаточно доказать теорему для предложений именно такой формы. Затем мы докажем теорему для предложений этой формы. Это делается путем первоначального замечания, что предложение такого вида либо опровержимо (его отрицание всегда истинно), либо выполнимо, то есть существует модель, в которой оно истинно (оно может быть даже всегда истинным, то есть быть тавтологией); такая модель просто присваивает значения истинности подформулам, из которых построено B. Это объясняется полнотой пропозициональной логики, при которой экзистенциальные кванторы не играют роли. Мы расширяем этот результат на все более сложные и длинные предложения Dn (n = 1, 2), построенные на основе B, так что либо хотя бы одно из них опровержимо, и, следовательно, опровержима и φ, либо ни одно из них не опровержимо, и, следовательно, каждое из них выполнимо в некоторой модели. Наконец, мы используем модели, в которых Dn выполнимы (в случае, если ни одно из них не опровержимо), для построения модели, в которой выполнима и φ.

Теорема 1. Каждая действительная формула (истинная во всех структурах) доказуема.

Это самая основная формулировка теоремы о полноте. Мы немедленно переформулируем её в виде, более удобном для наших целей: когда мы говорим "все структуры", важно уточнить, что речь идёт о классических (тарскианских) интерпретациях I, где I = <U, F> (U – непустое (возможно, бесконечное) множество объектов, а F – множество функций, отображающих выражения интерпретируемого символизма в U). [В отличие от этого, так называемые "свободные логики" допускают возможность пустого множества для U. Более подробную информацию о свободных логиках можно найти в работах Кареля Ламберта.]

Теорема 2. Каждая формула φ либо опровергаема, либо удовлетворяема в некоторой структуре.

"φ опровержимо" по определению означает "¬φ доказуемо".

Эквивалентность обоих теорем

Если теорема 1 верна, и φ не выполнима ни в одной структуре, то ¬φ истинна во всех структурах и, следовательно, доказуема, таким образом, φ опровержима, и теорема 2 верна. Если же теорема 2 верна, и φ истинна во всех структурах, то ¬φ не выполнима ни в одной структуре и, следовательно, опровержима; тогда ¬¬φ доказуема, а значит и φ доказуема, таким образом, теорема 1 верна.

Доказательство теоремы 2: первый шаг

Мы подходим к доказательству теоремы 2 путем последовательного ограничения класса всех формул φ, для которых нам нужно доказать, что "φ либо опровержима, либо выполнима". Вначале нам нужно доказать это для всех возможных формул φ в нашем языке. Однако, предположим, что для каждой формулы φ существует формула ψ, взятая из более ограниченного класса формул C, такая, что "ψ либо опровержима, либо выполнима" → "φ либо опровержима, либо выполнима". Затем, как только это утверждение (выраженное в предыдущем предложении) будет доказано, будет достаточно доказать, что "φ либо опровержима, либо выполнима" только для φ, принадлежащих классу C. Если φ доказуемо эквивалентна ψ (т.е. (φ ≡ ψ) является доказуемым), то действительно имеет место, что "ψ либо опровержима, либо выполнима" → "φ либо опровержима, либо выполнима" (теорема о корректности необходима для этого). Существуют стандартные методы преобразования произвольной формулы в формулу, которая не использует функциональные или константные символы, ценой введения дополнительных кванторов; поэтому мы будем считать, что все формулы не содержат таких символов. В работе Гёделя используется версия исчисления предикатов первого порядка, которая изначально не имеет функциональных или константных символов. Далее мы рассмотрим произвольную формулу φ (которая больше не использует функциональные или константные символы) и применим теорему о пренексной форме, чтобы найти формулу ψ в нормальной форме, такую что φ ≡ ψ (ψ в нормальной форме означает, что все кванторы в ψ, если они есть, находятся в самом начале ψ). Отсюда следует, что нам нужно доказать теорему 2 только для формул φ в нормальной форме. Далее мы устраняем все свободные переменные из φ, квантифицируя их экзистенциально: если, скажем, x1, ..., xn свободны в φ, мы формируем. Если ψ выполнима в структуре M, то, безусловно, выполнима и φ, а если ψ опровержима, то ⊥ доказуемо, и следовательно, ¬φ доказуемо, таким образом, φ опровержима. Мы видим, что мы можем ограничить φ предложением, то есть формулой без свободных переменных. Наконец, для технического удобства мы хотим, чтобы префикс φ (то есть строка кванторов в начале φ, которая находится в нормальной форме) начинался с универсального квантора и заканчивался экзистенциальным квантором. Чтобы достичь этого для произвольной φ (с учетом ограничений, которые мы уже доказали), мы берем одноместный реляционный символ F, не используемый в φ, и две новые переменные y и z. Если φ = (P)Φ, где (P) обозначает префикс φ, а Φ – матрицу (оставшуюся часть φ, не содержащую кванторов), мы формируем. Поскольку это явно доказуемо, легко увидеть, что это также доказуемо.

Доказательство теоремы для формул 1-й степени

Как показано выше, нам нужно доказать нашу теорему только для формул φ в R степени 1. Формула φ не может быть степени 0, поскольку формулы в R не имеют свободных переменных и не используют константные символы. Итак, формула φ имеет общий вид: теперь мы определяем порядок k-кортежей натуральных чисел следующим образом: должно выполняться, если либо , либо , и предшествует в лексикографическом порядке. [Здесь обозначает сумму элементов кортежа.] Обозначим n-й кортеж в этом порядке как . Зададим формулу как , а затем .

Лемма: Для любого n,
Доказательство: По индукции на n; мы имеем , где последнее включение выполняется посредством подстановки переменных, поскольку порядок кортежей таков, что . Но последняя формула эквивалентна φ. Для базового случая, очевидно, является следствием φ. Итак, лемма доказана. Теперь, если опровержимо для некоторого n, то следует, что φ опровержима. С другой стороны, предположим, что не опровержимо для любого n. Тогда для каждого n существует способ присвоить значения истинности различным подформулам (упорядоченным по их первому появлению в ; "различные" здесь означает либо различные предикаты, либо различные связанные переменные) в , таким образом, чтобы было истинно при такой оценке каждой подформулы. Это следует из полноты базовой пропозициональной логики. Теперь мы покажем, что существует такое присваивание значений истинности для , чтобы все были истинными: они появляются в одном и том же порядке в каждом ; мы индуктивно определим общее присваивание для них своего рода "принципом большинства": поскольку существует бесконечно много присваиваний (одно для каждого ), влияющих на , либо бесконечно много делают истинным, либо бесконечно много делают ложным, и только конечное число делают истинным. В первом случае мы выбираем истинным в общем случае; во втором – ложным в общем случае. Затем из бесконечного множества n, для которых через присвоены те же значения истинности, что и в общем присваивании, мы выбираем общее присваивание тем же способом. Это общее присваивание должно привести к тому, что каждое из и будет истинным, поскольку если бы одно из было ложным в соответствии с общим присваиванием, оно также было бы ложным для каждого n > k. Но это противоречит тому факту, что для конечного набора общих присваиваний, появляющихся в , существует бесконечно много n, где присваивание, делающее истинным, соответствует общему присваиванию. Из этого общего присваивания, которое делает все истинными, мы построим интерпретацию предикатов языка, которая делает φ истинной. Универсом модели будут натуральные числа. Каждый n-арный предикат должен быть истинным для натуральных чисел , именно тогда, когда подформула либо истинна в общем присваивании, либо не присвоена ему (потому что она никогда не появляется ни в одном из ). В этой модели каждая из формул истинна по построению. Но это подразумевает, что φ сама по себе истинна в модели, поскольку переменные пробегают все возможные k-кортежи натуральных чисел. Итак, φ выполнима, и мы закончили.

Интуитивное объяснение

Мы можем записать каждый Bi как Φ(x1 xk, y1 ym) для некоторых xs, которые мы можем назвать "первыми аргументами", и ys, которые мы можем назвать "последними аргументами". Возьмем, к примеру, B1. Его "последними аргументами" являются z2, z3, ..., zm+1, и для каждой возможной комбинации из k этих переменных существует такое j, что они появляются как "первые аргументы" в Bj. Таким образом, для достаточно больших n1, Dn1 обладает свойством, что "последние аргументы" B1 появляются, в каждой возможной комбинации из k элементов, как "первые аргументы" в других Bjs внутри Dn. Для каждого Bi существует Dni с соответствующим свойством. Следовательно, в модели, удовлетворяющей всем Dns, есть объекты, соответствующие z1, z2, ..., и каждая комбинация из k этих объектов появляется как "первые аргументы" в некотором Bj, что означает, что для каждого k этих объектов zp1, zp2, ..., zpk существуют zq1, zq2, ..., zqm, при которых Φ(zp1, zp2, ..., zpk, zq1, zq2, ..., zqm) истинно. Выбрав подмодель, состоящую только из этих объектов z1, z2, ..., мы получим модель, удовлетворяющую φ.

Расширение на предикатное исчисление первого порядка с равенством

Гёдель привел формулу, содержащую экземпляры предиката равенства, к формуле без них в расширенном языке. Его метод заключается в замене формулы φ, содержащей некоторые случаи равенства, формулой

Здесь обозначаются предикаты, встречающиеся в φ (с их соответствующими арностями), а φ' – это формула φ, в которой все вхождения равенства заменены новым предикатом Eq. Если эта новая формула опровержима, то и исходная φ была опровержима; то же самое верно и для выполнимости, поскольку можно рассмотреть фактор-модель выполнимой модели новой формулы по отношению эквивалентности, представляющему Eq. Этот фактор-модель корректно определена относительно остальных предикатов и, следовательно, будет удовлетворять исходной формуле φ.

Расширение на совокупности формул, которые можно сосчитать

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

Расширение произвольных наборов формул

Когда имеется несчетно бесконечное множество формул, требуется аксиома выбора (или, по крайней мере, некоторая её слабая форма). Используя полную аксиому выбора, можно установить линейный порядок на формулах и доказать случай с несчетным множеством тем же аргументом, что и для счетного множества, за исключением использования трансфинитной индукции. Другие подходы могут быть использованы для доказательства того, что в этом случае теорема о полноте эквивалентна теореме о булевых простых идеалах, являющейся слабой формой аксиомы выбора.