ГЁДЕЛЯ ТЕОРЕМА О НЕПОЛНОТЕ

ГЁДЕЛЯ ТЕОРЕМА О НЕПОЛНОТЕ - общее название двух теорем, установленных К. Гёделем [1]. Первая Г. т. о н. утверждает, что в любой непротиворечивой формальной системе, содержащей минимум арифметики (+, ⋅, знаки ∀, ∃ и обычные правила обращения с ними), найдется формально неразрешимое суждение, т. е. такая замкнутая формула А, что ни А, ни ¬А не являются выводимыми в системе. Вторая Г. т. о н. утверждает, что при выполнении естественных дополнительных условий в качестве А можно взять утверждение о непротиворечивости рассматриваемой системы. Эти теоремы знаменовали неудачу первоначального понимания программы Гильберта в области оснований математики, к-рая предусматривала полную формализацию всей существующей математики или значительной ее части (невозможность этого показала первая Г. т. о н.) и обоснование полученной формальной системы путем финитного доказательства ее непротиворечивости (вторая Г. т. о н. показала, что даже если финитными считаются все средства формализованной арифметики, этого не хватит уже для доказательства непротиворечивости арифметики).

Формально неразрешимое суждение строится методом арифметизации синтаксиса, к-рый стал одним из основных методов теории доказательств (метаматематики).

Фиксируется нумерация основных формальных объектов (формул, конечных последовательностей формул и т. д.) натуральными числами такая, что основные свойства этих объектов (быть аксиомой, быть выводом по правилам системы и т. д.) оказываются распознаваемыми по их номерам с помощью весьма простых алгоритмов. Столь же просто вычисляются по номерам исходных данных номера результатов комбинаторных преобразований (напр., подстановки терма в формулу вместо переменной). При этом оказывается возможным написать арифметич. формулу В(а, b), имеющую вид f(a, b) = 0 (f - примитивно рекурсивная функция) и выражающую условие: b есть номер формулы, к-рая получается из формулы с номером а путем подстановки натурального числа а вместо переменной х. Если р -номер формулы ∀b¬B(x, b), то формула ∀b¬B(р, b) выражает свою собственную невыводимость. Она и оказывается формально неразрешимой. Отсюда следует, что в любой непротиворечивой системе с минимальными выразительными арифметическими возможностями имеется истинное, но не выводимое суждение указанного вида.

Вторая Г. т. о н. получается путем формализации доказательства первой Г. т. о н. Ее доказательство существенно использует особенности арифметизации синтаксиса рассматриваемой системы, а именно - требуется выводимость в этой системе формул, выражающих суждения: 1) система замкнута относительно правила сокращения посылки (модус поненс); 2) система замкнута относительно подстановки термов вместо предметных переменных; 3) из истинности формулы вида f(N) = 0, где N - натуральное число, f - примитивно рекурсивная функция, следует ее выводимость. Эти условия выполняются для естественной арифметизации, но можно, не меняя алгорифмич. характеристик арифметизации (все функции и предикаты остаются примитивно рекурсивными), изменить ее так, что формула, выражающая непротиворечивость системы (применительно к новой арифметизации), будет выводима. При этом для новой арифметизации будет нарушено условие 1).

Вторая Г. т. о н. дает критерий сравнения формальных систем: если в системе S можно доказать непротиворечивость системы Т, то S не погружается в Т (см. Погружающая операция). Так, доказывается, что формальный математический анализ не погружается в арифметику, типов теория не погружается в анализ, теория множеств Z не погружается в теорию типов.

Лит.: [1] Gödel К., «Monatshefte für Math. und Phys.», 1931, Bd 38, S. 173-98; [2] Hilbert D., Bernays P., Grundlagen der Mathematik, 2 Aufl., Bd 2, В., 1970; [3] Клини С. К., Введение в метаматематику, пер. с англ., М., 1957.

Г. Е. Минц.

Источники:

1. Математическая Энциклопедия. Т. 1 (А - Г). Ред. коллегия: И. М. Виноградов (глав ред) [и др.] - М., «Советская Энциклопедия», 1977, 1152 стб. с илл.