Подчеркнем: именно эта часть аргументации Гёделя зависит в основном от того факта, что программа Гильберта допускает только доказательства, проверяемые алгоритмически. Если бы были разрешены другие методы рассуждения (поговорим о них в следующей главе), то не было бы возможности гарантировать, что свойство "х — это код доказуемого высказывания" может быть выражено в арифметических терминах.
Все принципы математики сводятся к принципам логики.
Уиллард ван Орман Куайн. "С точки зрения логики"
Как Гёдель доказал, что понятие доказуемости можно выразить? Для начала он доказал, что любое числовое свойство, проверяемое алгоритмически (например, "быть простым числом", "быть четным" или "делиться на 9"), всегда можно выразить с помощью сумм, произведений и логических операций.
Итак, то, что высказывание Р доказуемо, означает, что существует доказательство (принимаемое программой Гильберта), в котором Р — это конечное высказывание. В качестве примера мы уже приводили доказательство того, что "4 = 2 + 2" на основе аксиом "S(x + у) = х + S(y)" и "х + 1 = S(x)". Вспомним, что этому доказательству, с учетом последовательности высказываний, соответствует число Гёделя 2414871965597. Вспомним также, что "4 = 2 + 2" соответствует число 67. В переводе на язык кодов доказуемость "4 = 2 + 2" означает, что существует конечная последовательность высказываний (ее код 2414871965597), являющаяся доказательством, в котором конечное высказывание имеет код 67.
"Быть кодом доказательства" — это свойство, проверяемое алгоритмически, поскольку при заданном коде для осуществления проверки компьютер сначала использовал бы программу, восстанавливающую последовательность высказываний, соответствующую этому коду, а затем применил бы к этой последовательности высказываний алгоритм, который определяет, идет ли речь о доказательстве:
Код последовательности → Последовательность высказываний → Это доказательство?
НАЙТИ ИЛИ ПРОВЕРИТЬ
Теория доказательства ставит две проблемы, которые хоть и схожи, но не должны смешиваться. Первая заключается в том, чтобы при данном высказывании Р найти его доказательство (или доказать, что его не существует). Вторая — в том, чтобы определить, верно ли предложенное доказательство. Вторая проблема может быть сложной, но первая намного сложнее. Если методы доказательства подходящие, то вторая проблема может быть решена алгоритмически. Проблема нахождения доказательства, наоборот, неразрешима таким образом.
Британский математик Эндрю Уайлс.
Последняя теорема Ферма
В качестве примера можно рассмотреть последнюю теорему Ферма.
В 1637 году Пьер Ферма записал, что если n > 2, то уравнение х>n + у>n = z>n не имеет решений для натуральных чисел. Ферма уверял, что у него есть доказательство этого факта, но так и не привел его. Проблема нахождения доказательства последней теоремы Ферма стала широко известной и в конце концов была решена Эндрю Уайлсом в 1996 году (он представил первое доказательство в 1995 году, но выяснилось, что в нем содержится ошибка, которая была исправлена почти через год). Определение правильности доказательства Уайлса потребовало несколько дней усилий; но для нахождения доказательства понадобилось более 350 лет.
Каждый шаг может осуществляться алгоритмически.
Следовательно, при заданных х и у свойство "у — это код доказательства, которое заканчивается высказыванием с кодом х" также является свойством, проверяемым алгоритмически, поскольку к предыдущей процедуре надо добавить только проверку того, что последовательность заканчивается высказыванием, соответствующим числу Гёделя х. Поскольку свойство проверяется алгоритмически, пропозициональную функцию "у — это код доказательства, которое заканчивается высказыванием с кодом х" можно выразить в терминах сумм, произведений и логических операций.
Наконец, делаем вывод, что выражение "существует некое у у являющееся кодом доказательства, заканчивающегося высказыванием с кодом х" также можно выразить арифметическими терминами. Фактически в этом утверждении говорится, что существует некое доказательство высказывания с кодом х