3.6. Теоремы ограничения в формальных системах

Вторая теорема Геделя была первой теоремой ограничения и произвела огромное впечатление одновременно и на математиков, и на философов. Она не была единственной теоремой ограничения. Ниже мы приведем еще две теоремы ограничения (Тарского и Черча), имеющие большое теоретическое и практическое значение.

Теорема Тарского (1935 г.)

Существуют формальные системы, для которых всякая интерпретация приводит к выражениям одновременно истинным и недоказуемым.

Эта теорема является парной (относительно интерпретаций) ко второй теореме Геделя. В сжатом виде она формулируется так: что истинно, всегда недоказуемо” или же “понятие истинности неформализуемо”. Теорема говорит, что в каждой интерпретации существует по крайней мере одна формула, всегда интерпретируемая как ИСТИНА, которая однако не является теоремой данной формальной системы.

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

Теорема Черча (1936 г.)

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

Следовательно, существуют неразрешимые формальные системы. Иначе говоря, для некоторых формальных систем

невозможно построить системы процедур, позволяющих отличать теоремы от не-теорем. Такие системы называются неразрешимыми, или говорят, что они не являются рекурсивно перечислимыми. Конечно, хотелось бы обойтись без таких формальных систем, но это невозможно, тем более, что уже исчисление предикатов первого порядка, как показал Черч, является неразрешимым. Тем более неразрешимой является более мощная формальная система, представленная в “Основаниях математики” Рассела и Уайтхеда. Тарский показал также, что теории групп, колец и тел являются неразрешимыми, а проективная геометрия в пространстве вещественных чисел и теория вещественных :<;замкнутых тел являются разрешимыми. Кроме того, доказано,что по исчисление предикатов первого порядка является полуразрешимым, т. е. для выражений которые эффективно являются теоремами, имеется конечная процедура, которая их доказывает. Все эти доказательства основываются на определении процедур решения. Черч идентифицировал понятие эффективной или вычислимой процедуры, т. е. алгоритма, или функциональной рекурсивной процедуры (“тезис” Черча).

Независимо от других в 1937 г. Тьюринг формализовал идею вычислительной машины и свел проблему разрешимости к проблеме останова идеальной вычислительной машины (см. разд. 5.11). Оба подхода оказались в результате идентичными, и было показано, что в общем случае не существует ни рекурсивной функции, ни машины Тьюринга, с помощью которых можно было бы определить, является ли какая-то заданная формула теоремой (или не является) в данной формальной системе (или в данном “языке”). В частности, неразрешима проблема останова программы, выполняемой на машине Тьюринга.

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

Некоторые философы и специалисты по теории информации, как, например, Ж. Лука, Е. Нагель и Д. Ньюман, пытались применить теоремы ограничения к проблемам обработки символьной информации на ЭВМ. Основываясь на этих теоремах, они сделали, на мой взгляд, несколько преждевременный вывод о превосходстве интеллекта человека над машиной. Подобные

аргументы до сих пор используются, чтобы дискредитировать все исследования по искусственному интеллекту. На самом деле результаты, полученные Геделем, Тарским и Черчем, говорят только о том, что некоторые задачи неразрешимы средствами современной математики. Эти ограничения относятся к людям в той же степени, что и к ЭВМ, так же касаются математиков, как и машинных программ. И тем не менее это не привело начиная с 1930 г. когда эти теоремы были доказаны, к свертыванию математических исследований (наоборот, к их расширению). Некоторые задачи решить невозможно, но зато другие задачи заслуживают того, чтобы их решили. Кроме того, знание задач, которые являются трудноразрешимыми, открывает новые пути для поисков. Гипотезы Гольдбаха, великая “теорема” Ферма по-прежнему еще не классифицированы (не определено, являются ли они доказуемыми или неразрешимыми). Вторая задача Гильберта, сформулированная наряду с 22 другими в 1905 г. (найти метод решения для произвольного уравнения в целых числах) была снята с повестки дня в 1970 г. Матиасевич доказал ее неразрешимость.

Знаменитая проблема четырех цветов (раскрасить географическую карту, используя только четыре различных цвета, причем так, чтобы любые две соседние страны имели различные цвета) (гл. 5) была разрешена с помощью ЭВМ в 1976 г. Аппелем и Хакеном спустя более 120 лет после того, как она была поставлена Ф. Гутри.

Если задача вам кажется очень трудной, удостоверьтесь сначала, что она не относится к одному из известных случаев неразрешимости, и если это не так, то не отказывайтесь от нее слишком быстро!

В заключение приведем формулировки теорем ограничения: Возможны формальные системы, в которых

• существуют формулы такие, что ни ни не являются доказуемыми (теорема Геделя);

• во всякой их интерпретации найдутся выражения, истинные, но недоказуемые (теорема Тарского);

• не существует алгоритма, чтобы отличать теоремы от не-теорем (теорема Черча).