Теорема Гёделя о неполноте
Теорема Гёделя о неполноте
Общее название двух теорем, установленных К. Гёделем. Первая теорема Геделя утверждает, что в любой непротиворечивой формальной системе, содержащей минимум арифметики (+, ∙ знаки ∀,∃ и обычные правила обращения с ними), найдется формально неразрешимое суждение, т. е. такая замкнутая формула А, что ни А, ни ¬A не являются выводимыми в системе.
Вторая теорема Геделя утверждает, что при выполнении естественных дополнительных условий в качестве А можно взять утверждение о непротиворечивости рассматриваемой системы.
Эти теоремы знаменовали неудачу первоначального понимания программы Гильберта в области оснований математики, которая предусматривала полную формализацию всей существующей математики или значительной ее части (невозможность этого показала первая теорема Геделя) и обоснование полученной формальной системы путем, финитного доказательства ее непротиворечивости (вторая теорема Геделя показала, что даже если финитными считаются все средства формализованной арифметики, этого не хватит уже для доказательства непротиворечивости арифметики).
Формально неразрешимое суждение строится методом арифметизации синтаксиса, который стал одним из основных методов теории доказательств (метаматематики).
Фиксируется нумерация основных формальных объектов (формул, конечных последовательностей формул и т. д.) натуральными числами такая, что основные свойства этих объектов (быть аксиомой, быть выводом по правилам системы и т. д.) оказываются распознаваемыми по их номерам с помощью весьма простых алгоритмов.
Столь же просто вычисляются по номерам исходных данных номера результатов комбинаторных преобразований (например, подстановки терма в формулу вместо переменной). При этом оказывается возможным написать арифметическую формулу В( а,b), имеющую вид f(a,b) = 0 (f - примитивно рекурсивная функция) и выражающую условие: b есть номер формулы, которая получается из формулы с номером а путем подстановки натурального числа а вместо переменной х.
Если р - номер формулы ∀b¬B(x,b), то формула ∀b¬B(p,b) выражает свою собственную невыводимость. Она и оказывается формально неразрешимой.
Отсюда следует, что в любой непротиворечивой системе с минимальными выразительными арифметическими возможностями имеется истинное, но не выводимое суждение указанного вида. Вторая теорема Геделя получается путем формализации доказательства первой теоремы Геделя. Ее доказательство существенно использует особенности арифметизации синтаксиса рассматриваемой системы, а именно - требуется выводимость в этой системе формул, выражающих суждения:
1) система замкнута относительно правила сокращения посылки;
2) система замкнута относительно подстановки термов вместо предметных переменных;
3) из истинности формулы вида f(N)=0, где N - натуральное число, f - примитивно рекурсивная функция, следует ее выводимость.
Эти условия выполняются для естественной арифметизации, но можно, не меняя алгоритмических характеристик арифметизации (все функции и предикаты остаются примитивно рекурсивными), изменить ее так, что формула, выражающая непротиворечивость системы (применительно к новой арифметизации), будет выводима. При этом для новой арифметизации будет нарушено условие 1). Вторая теорема Геделя дает критерий сравнения формальных систем: если в системе Sможно доказать непротиворечивость системы Т, то S не погружается в Т. Так, доказывается, что формальный математический анализ не погружается в арифметику, типов теория не погружается в анализ, теория множеств Z не погружается в теорию типов.
Столь же просто вычисляются по номерам исходных данных номера результатов комбинаторных преобразований (например, подстановки терма в формулу вместо переменной). При этом оказывается возможным написать арифметическую формулу В( а,b), имеющую вид f(a,b) = 0 (f - примитивно рекурсивная функция) и выражающую условие: b есть номер формулы, которая получается из формулы с номером а путем подстановки натурального числа а вместо переменной х.
Если р - номер формулы ∀b¬B(x,b), то формула ∀b¬B(p,b) выражает свою собственную невыводимость. Она и оказывается формально неразрешимой.
Отсюда следует, что в любой непротиворечивой системе с минимальными выразительными арифметическими возможностями имеется истинное, но не выводимое суждение указанного вида. Вторая теорема Геделя получается путем формализации доказательства первой теоремы Геделя. Ее доказательство существенно использует особенности арифметизации синтаксиса рассматриваемой системы, а именно - требуется выводимость в этой системе формул, выражающих суждения:
1) система замкнута относительно правила сокращения посылки;
2) система замкнута относительно подстановки термов вместо предметных переменных;
3) из истинности формулы вида f(N)=0, где N - натуральное число, f - примитивно рекурсивная функция, следует ее выводимость.
Эти условия выполняются для естественной арифметизации, но можно, не меняя алгоритмических характеристик арифметизации (все функции и предикаты остаются примитивно рекурсивными), изменить ее так, что формула, выражающая непротиворечивость системы (применительно к новой арифметизации), будет выводима. При этом для новой арифметизации будет нарушено условие 1). Вторая теорема Геделя дает критерий сравнения формальных систем: если в системе Sможно доказать непротиворечивость системы Т, то S не погружается в Т. Так, доказывается, что формальный математический анализ не погружается в арифметику, типов теория не погружается в анализ, теория множеств Z не погружается в теорию типов.
2012-12-21 • Просмотров [ 1482 ]
