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

общее название двух теорем, установленных К. Гёделем [1]. Первая Г. Т. О н. Утверждает, что в любой непротиворечивой формальной системе, содержащей минимум арифметики ( знаки и обычные правила обращения с ними), найдется формально неразрешимое суждение, т. Е. Такая замкнутая формула А, что ни А, ни не являются выводимыми в системе. Вторая Г. Т. О н. Утверждает, что при выполнении естественных дополнительных условий в качестве Аможно взять утверждение о непротиворечивости рассматриваемой системы. Эти теоремы знаменовали неудачу первоначального понимания программы Гильберта в области оснований математики, к-рая предусматривала полную формализацию всей существующей математики или значительной ее части (невозможность этого показала первая Г.

Т. О н.) и обоснование полученной формальной системы путем .финитного доказательства ее непротиворечивости (вторая Г. Т. О н. Показала, что даже если финитными считаются все средства формализованной арифметики, этого не хватит уже для доказательства непротиворечивости арифметики). Формально неразрешимое суждение строится методом арифметизации синтаксиса, к-рый стал одним из основных методов теории доказательств (метаматематики). Фиксируется нумерация основных формальных объектов (формул, конечных последовательностей формул и т. Д.) натуральными числами такая, что основные свойства этих объектов (быть аксиомой, быть выводом по правилам системы и т. Д.) оказываются распознаваемыми по их номерам с помощью весьма простых алгоритмов.

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

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

При этом для новой арифметизации будет нарушено условие 1). Вторая Г. Т. О н. Дает критерий сравнения формальных систем. Если в системе Sможно доказать непротиворечивость системы Т, то Sне погружается в Т(см. Погружающая операция). Так, доказывается, что формальный математический анализ не погружается в арифметику, типов теория не погружается в анализ, теория множеств Zне погружается в теорию типов. Лит.:[1] Godе1 К., "Monatshefte fur Math, und Phys.", 1931, Bd 38, S. 173-98. [2] Hi1bеrt D., Веrnауs P, Grundlagcn der Mathematik, 2 Aufl., Bd 2, В., 1970. [3] Клини С. К., Введение в метаматематику, пер. С англ., М., 1957. Г. Е. Минц.