Роджер Пенроуз - Новый ум короля: О компьютерах, мышлении и законах физики
Гильберт рассчитывал, что для любой строки символов, представляющих математическое утверждение, скажем, Р, можно будет доказать либо Р, либо ~ Р, если Р истинно или ложно, соответственно. Здесь мы в обязательном порядке оговариваем, что строка должна быть синтаксически корректна, где «синтаксически корректна» по сути означает «грамматически корректна» — то есть удовлетворяет всем правилам записи, принятым в данном формализме, среди которых будет правильное попарное соответствие скобок и т. п. — так чтобы Р всегда имело четко определенное значение «ложь» или «истина». Если бы надежды Гильберта оправдались, то можно было бы вообще не задумываться о том, что означает то или иное утверждение! Р было бы просто-напросто синтаксически корректной строкой символов. Строке было бы приписано значение ИСТИНА, если бы Р являлось теоремой (другими словами, если бы Р было доказуемо в рамках системы); или же ЛОЖЬ, если бы теоремой было ~ Р. Чтобы такой подход имел смысл, мы должны дополнительно к условию полноты наложить еще и условие непротиворечивости, гарантирующее отсутствие такой строки символов Р, для которой как Р, так и ~ Р были бы теоремами. Ведь в противном случае Р могло бы быть одновременно и ИСТИНОЙ, и ЛОЖЬЮ!
Такой подход, согласно которому можно пренебрегать смысловыми значениями математических выражений и рассматривать их лишь как строки символов некоторой формальной математической системы, в математике получил название формализма. Некоторым нравится эта точка зрения, с которой математика превращается в своего рода «бессмысленную игру». Однако я сам не являюсь сторонником таких идей. Все-таки именно «смысл» — а не слепые алгоритмические вычисления — составляет сущность математики. К счастью, Гедель нанес формализму сокрушающий удар! Давайте посмотрим, как он это сделал.
Теорема Геделя
Часть доказательства, приведенного Геделем, содержало некий очень сложный и детализированный кусок. Однако нам не обязательно разбираться во всех его тонкостях. Основная идея, в то же время, была проста, красива и глубока. И ее мы сможем оценить по достоинству. В «сложной» части (которая, впрочем, содержит много остроумных рассуждений) подробно показано, каким образом частные правила вывода и использование различных аксиом формальной процедуры могут быть представлены в виде арифметических операций. (Хотя в сложной части становится понятной плодотворность этих действий!) Для этого представления нам необходимо будет найти какой-нибудь удобный способ нумерации утверждений при помощи натуральных чисел. Один из способов мог бы заключаться в том, чтобы использовать своего рода «алфавитный» порядок для строчек символов формальной системы, имеющих одинаковую длину, упорядочить заранее строчки по длине. (Таким образом, за выстроенными в алфавитном порядке строками из одного символа будут следовать строки длиной в два символа, также упорядоченные по алфавиту; за ними идут строки из трех символов и так далее.) Это называется лексикографическим порядком[72]. В действительности Гедель использовал более сложную систему нумерации, но различия в данном случае для нас несущественны. Нас же должны в особенности интересовать функции исчисления высказываний одной переменной, наподобие введенной выше G(ω). Пусть n-я (из пронумерованных выбранным способом строк символов) такая функция от аргумента ω обозначается
Pn(ω).
Мы можем допустить, чтобы наша нумерация по желанию была несколько «либеральна» в отношении синтаксически некорректных выражений. (Это позволит значительно упростить перевод системы на язык арифметических операций по сравнению со случаем, когда мы будем стараться исключить из рассмотрения синтаксически некорректные выражения.) Если Pn(ω) синтаксически корректно, то оно будет представлять из себя некоторое совершенно определенное арифметическое выражение, в котором фигурируют два натуральных числа п и ад. Каков будет конкретный вид этого выражения — зависит от особенностей системы нумерации, которую мы выбрали. Но эти детали рассматриваются в «сложной» части и сейчас нас не касаются. Пусть Пn будет n-м доказательством. (Опять же мы можем использовать «либеральную нумерацию», когда для некоторых значений n выражение Пn не является синтаксически корректным и, тем самым, не доказывает никакую теорему.)
А теперь рассмотрим следующую функцию исчисления высказываний от натурального числа ω :
— Eк.с.x[Пx доказывает Pω(ω)].
В выражении в квадратных скобках частично присутствуют слова, но, тем не менее, это — абсолютно точно определенное выражение. Оно говорит о том, что доказательство номер х является доказательством утверждения Рω(), примененного к самому ω. Находящийся за скобками квантор существования с отрицанием позволяет исключить из рассмотрения одну из переменных («не существует такого х, что…»), приводя нас в конечном счете к арифметической функции исчисления высказываний, зависящей только от ω. В целом данное выражение утверждает, что не существует доказательства Рω(ω). Я буду предполагать, что оно оформлено синтаксически корректным образом (даже если Рn(ω) некорректно — поскольку тогда выражение было бы истинным за невозможностью существования доказательства синтаксически некорректного утверждения). На самом деле, в результате сделанного нами перевода на язык арифметики, написанное выше будет в действительности неким арифметическим выражением, включающим натуральное число ω (тогда как в квадратных скобках окажется четко определенное арифметическое выражение, связывающее два натуральных числа х и ω). Конечно, возможность представления этого выражения в арифметическом виде далеко не очевидна, но она существует. Рассуждения, приводящие к этому заключению, составляют наиболее трудную задачу в «сложной» части доказательства Геделя. Как и ранее, непосредственный вид арифметического выражения будет зависеть от способа нумерации и в еще большей степени от конкретной структуры аксиом и правил вывода, принятых в нашей системе. Поскольку все это входит в «сложную» часть доказательства, то в данном случае нас не интересует.
Мы пронумеровали все функции исчисления высказываний, зависящие от одной переменной, поэтому той, которую мы ввели выше, также должен быть приписан номер. Пусть этот номер будет k. Наша функция будет в таком случае k-й в общем списке. То есть
— Eк.с.x[Пх доказывает Pω(ω)] = Рk(ω).
Теперь исследуем эту функцию при определенном значении: ω = k. Мы получаем:
Eк.с. х[Пх доказывает Pk(k)] = Pk(k)
Данное утверждение Pk(k) является абсолютно точно определенным (синтаксически корректным) арифметическим выражением. Может ли оно быть доказано в рамках нашей формальной системы? А его отрицание ~ Pk(k) — имеет ли оно такое доказательство? Ответ в обоих случаях будет отрицательный. Мы можем убедиться в этом путем исследования смысла, который лежит в основании процедуры Геделя. Хотя Pk(k) является просто арифметическим выражением, последнее было построено нами таким образом, что написанное в левой части утверждает следующее: «внутри системы не существует доказательства Pk(k)». Если мы были аккуратны в определении аксиом и процедур вывода, и не ошиблись при нумерации, то тогда в рамках системы такого доказательства найти невозможно. Если же доказательство существует, то значение утверждения, содержащегося в Pk(k) — о том, что такого доказательства нет, — будет ложным, а вместе с ним будет ложным и арифметическое выражение, отвечающее Pk(k). Но наша формальная система не может быть построена настолько плохо, чтобы включать в себя ложные утверждения, которые могут быть доказаны! Таким образом, в действительности, доказательство Pk(k) быть не может. Но это в точности то самое, о чем говорит нам Pk(k). То, что утверждает Pk(k), обязано, следовательно, быть верным, а поэтому Pk(k) должно быть верным как арифметическое выражение. Значит, мы нашли истинное утверждение, которое недоказуемо в рамках системы!
