А теперь рассмотрим следующую функцию исчисления высказываний от натурального числа ω :

— E_к.с.x[П_x доказывает P_ω(ω)].

В выражении в квадратных скобках частично присутствуют слова, но, тем не менее, это — абсолютно точно определенное выражение. Оно говорит о том, что доказательство номер х является доказательством утверждения Р_ω(), примененного к самому ω. Находящийся за скобками квантор существования с отрицанием позволяет исключить из рассмотрения одну из переменных («не существует такого х, что…»), приводя нас в конечном счете к арифметической функции исчисления высказываний, зависящей только от ω. В целом данное выражение утверждает, что не существует доказательства Р_ω(ω). Я буду предполагать, что оно оформлено синтаксически корректным образом (даже если Р_n(ω) некорректно — поскольку тогда выражение было бы истинным за невозможностью существования доказательства синтаксически некорректного утверждения). На самом деле, в результате сделанного нами перевода на язык арифметики, написанное выше будет в действительности неким арифметическим выражением, включающим натуральное число ω (тогда как в квадратных скобках окажется четко определенное арифметическое выражение, связывающее два натуральных числа х и ω). Конечно, возможность представления этого выражения в арифметическом виде далеко не очевидна, но она существует. Рассуждения, приводящие к этому заключению, составляют наиболее трудную задачу в «сложной» части доказательства Геделя. Как и ранее, непосредственный вид арифметического выражения будет зависеть от способа нумерации и в еще большей степени от конкретной структуры аксиом и правил вывода, принятых в нашей системе. Поскольку все это входит в «сложную» часть доказательства, то в данном случае нас не интересует.

Мы пронумеровали все функции исчисления высказываний, зависящие от одной переменной, поэтому той, которую мы ввели выше, также должен быть приписан номер. Пусть этот номер будет k. Наша функция будет в таком случае k-й в общем списке. То есть

— E_к.с.x[П_х доказывает P_ω(ω)] = Р_k(ω).

Теперь исследуем эту функцию при определенном значении: ω = k. Мы получаем:

E_к.с. х[П_х доказывает P_k(k)] = P_k(k)

Данное утверждение P_k(k) является абсолютно точно определенным (синтаксически корректным) арифметическим выражением. Может ли оно быть доказано в рамках нашей формальной системы? А его отрицание ~ P_k(k) — имеет ли оно такое доказательство? Ответ в обоих случаях будет отрицательный. Мы можем убедиться в этом путем исследования смысла, который лежит в основании процедуры Геделя. Хотя P_k(k) является просто арифметическим выражением, последнее было построено нами таким образом, что написанное в левой части утверждает следующее: «внутри системы не существует доказательства P_k(k)». Если мы были аккуратны в определении аксиом и процедур вывода, и не ошиблись при нумерации, то тогда в рамках системы такого доказательства найти невозможно. Если же доказательство существует, то значение утверждения, содержащегося в P_k(k) — о том, что такого доказательства нет, — будет ложным, а вместе с ним будет ложным и арифметическое выражение, отвечающее P_k(k). Но наша формальная система не может быть построена настолько плохо, чтобы включать в себя ложные утверждения, которые могут быть доказаны! Таким образом, в действительности, доказательство P_k(k) быть не может. Но это в точности то самое, о чем говорит нам P_k(k). То, что утверждает P_k(k), обязано, следовательно, быть верным, а поэтому P_k(k) должно быть верным как арифметическое выражение. Значит, мы нашли истинное утверждение, которое недоказуемо в рамках системы!

А как насчет ~ P_k(k)? Из предыдущих рассуждений видно, что доказательство этому утверждению внутри системы мы найти не сможем. Мы только что установили, что ~ P_k(k) должно быть ложным (ибо P_k(k) является истинным), а мы, по определению, не имеем возможности доказывать ложные утверждения в рамках системы! Таким образом, ни P_k(k), ни ~ P_k(k) недоказуемы в нашей формальной системе, что и составляет теорему Геделя.

Обратите внимание, что мы здесь сталкиваемся с одной примечательной особенностью. Часто думают, что теорема Геделя имеет, в некотором роде, отрицательный смысл, поскольку она указывает на принципиальные ограничения в применении формальных математических рассуждений. Независимо от нашего мнения об универсальности применяемого подхода, всегда найдутся утверждения, которые не попадают в сферу его действия. Но насколько, в действительности, нас могут затрагивать частные случаи типа P_k(k)? В ходе предыдущих рассуждений мы установили, что P_k(k) — истинное утверждение! Мы смогли это сделать несмотря на то, что это утверждение формально недоказуемо в рамках системы. А вот математических формалистов это должно волновать, потому что наши рассуждения с необходимостью приводят к выводам о неполноте их понятия «истины». Какая бы (непротиворечивая) формальная система не использовалась для арифметики, в ней будут содержаться утверждения, понимаемые нами как истинные, но которым не может быть приписано значение ИСТИНА при помощи вышеописанной формальной процедуры. Способ, при помощи которого формалист сумел бы обойти подобные трудности, мог бы состоять в том, чтобы не говорить о понятии истины, а только лишь о доказуемости внутри конкретной формальной системы. Однако же, такой подход весьма ограничен. Он не позволил бы даже сформулировать утверждение Геделя и осуществить его доказательство, как это было сделано выше, поскольку в значительной части рассуждений речь идет как раз об определении того, что есть ложь, а что — истина[73]. Некоторые формалисты встают на более «прагматическую» точку зрения, заявляя, что их не волнуют утверждения, подобные P_k(k), поскольку они исключительно сложны и не интересны в качестве арифметических выражений. Отстаивают они свою точку зрения примерно так:

Несомненно, что утверждения вида P_k(k), будучи полностью выписанными, были бы чрезвычайно громоздки и выглядели бы странно для числовых математических выражений. Однако за последнее время были выдвинуты сравнительно простые выражения приемлемого с точки зрения математики характера, которые эквивалентны утверждениям Геделя[74]. Они недоказуемы на основании обычных аксиом арифметики, однако же следуют из некоего свойства «самоочевидности», которым обладает сама система аксиом.