Ǝ у ∀ x ~ Dem(x, y) ﬤ ∀ x ~ Dem(x, sub(n, 13, n)),
которую можно было бы теперь сокращенно обозначить через «A ﬤ G». Именно для этой формулы можно установить ее формальную доказуемость, но мы не будем здесь пытаться это делать.
Покажем лишь, что формула А недоказуема. Допустим противное. Тогда, поскольку формула A ﬤ G доказуема, modus ponens позволяет нам заключить, что доказуемой должна бы быть и формула G. Но если наше исчисление непротиворечиво, G формально неразрешима, а потому, конечно, недоказуема. Таким образом, если арифметика непротиворечива, то формула А недоказуема.
Что это означает? Формула А представляет метаматематическое высказывание «Арифметика непротиворечива». Значит, если бы высказывание можно было обосновать каким нибудь рассуждением, отобразимым в последовательность формул, являющуюся доказательством в арифметическом исчислении, сама формула А была бы доказуема. Но это, как мы только что видели, невозможно, если во всяком случае считать, что арифметика непротиворечива. Мы дошли, наконец, до заключительного аккорда: нам приходится согласиться, что если арифметика непротиворечива, то непротиворечивость ее не может быть установлена никаким метаматематическим рассуждением, допускающим представление в арифметическом формализме
Надо сказать, что этот замечательный результат проведенного Гёделем анализа проблемы не исключает, однако, возможности метаматематического доказательства непротиворечивости арифметики. Из него следует лишь, что невозможно такое доказательство непротиворечивости, которое могло бы быть отображено (переведено) в формальное доказательство, проводимое внутри самой формальной арифметики.
Положение здесь очень напоминает то, которое сложилось в геометрии в связи о доказательством невозможности деления произвольного угла на три части о помощью циркуля и линейки. Доказательство это отнюдь не исключает возможности произвести искомое деление при помощи каких-либо более сильных средств. И действительно, его можно осуществить, добавив к циркулю и линейке ещё постоянный эталон длины.
На самом деле метаматематические доказательства непротиворечивости арифметики были получены; первым такое доказательство осуществил представитель школы Гильберта Герхард Генцен в 1936 г., а впоследствии было получено еще несколько доказательств того же результата. Доказательства эти имеют большую логическую ценность, заключающуюся хотя бы уже в том, что они продемонстрировали существенно новые формы метаматематических рассуждений и конструкций, а также в том, что благодаря им выяснилось, какие новые виды правил вывода надо допустить, если мы хотим установить непротиворечивость арифметики. Но все подобные доказательства уже не могут быть воспроизведены в рамках арифметического исчисления, и, поскольку все новые правила вывода уже не являются финитистскими, доказательства непротиворечивости, полученные с их помощью, никоим образом нельзя считать достижением цели, поставленной в гильбертовской программе в ее первоначальной формулировке.
Заключительные замечания
Выводы, к которым пришел Гёдель, имеют ряд важных следствий, безусловно, не оцененных еще в достаточной мере. Выводы эти показывают прежде всего, что решение задачи отыскания для каждой дедуктивной системы (и в частности, для системы, в которой можно было бы выразить всю совокупность арифметических теорем) абсолютного доказательства непротиворечивости, удовлетворяющего предложенным Гильбертом «финитистским» критериям, если и не является логически невозможным (хотя бы в силу некоторой неопределенности самого понятия «финитности»), то во всяком случае в высшей степени маловероятно. Выводы эти показывают также, что имеется бесконечно много истинных арифметических предложений, которые нельзя формально вывести из произвольной данной системы аксиом посредством некоторого точного перечня правил вывода. Отсюда следует, что аксиоматический подход к арифметике натуральных чисел, кроме всего прочего, не в состоянии охватить всю область истинных арифметических суждений. Отсюда также вытекает, что то, что мы понимаем под процессом математического доказательства, не сводится к использованию аксиоматического метода. Формализованные аксиоматические процедуры доказательств основаны на некотором множестве выделенных и фиксированных с самого начала аксиом и правил вывода. Как видно уже из самих рас- суждений, использованных в гёделевских доказательствах, изобретательность математиков в деле отыскания новых правил доказательства не поддается никаким априорным ограничениям. Таким образом, совершенно безнадежно рассчитывать на то, что понятию убедительного математического доказательства можно придать раз навсегда четко очерченные логические формы. В связи со всем этим возникает целый ряд новых проблем, далеко еще не решенных и слишком трудных для подробного рассмотрения их здесь — независимо от того, можно ли рассчитывать на то, что понятия математической и логической истинности можно исчерпывающим образом определить или же (мнение, к которому стал склоняться сам Гёдель) такое определение находится в компетенции безоговорочного философского «реализма» платонистского толка.
Платонизм (реализм) — доктрина, согласно которой математика не творит и не придумывает рассматриваемые в ней «объекты», а открывает их, подобно тому как, например, Колумб открыл Америку. Таким образом, согласно этой точке зрения, объекты должны в некотором смысле «существовать» до их «открытия». Платонистская доктрина не предполагает, что объекты математического исследования находятся между собой в пространственно-временных отношениях. Обьекты эти суть отделенные от материальных оболочек вечные Формы, прототипы, населяющие особые абстрактные Сферы, доступные лишь Интеллекту. Согласно такой концепции треугольные или круглые формы физических предметов, данные нам в ощущениях, сами по себе вовсе не являются объектами математического исследования. Эти пространственные формы суть лишь несовершенные воплощения единого «совершенного» Треугольника или «совершенного» Круга, вечных, неизменных, лишь частично проявляющихся в облике материальных предметов и являющихся подлинными объектами рассмотрения математической мысли. Сам Гёдель обнаружил близость к такого рода воззрениям, заявляя, «что допущение… классов и общих понятий столь же законно, как и допущение физических тел… и имеются столь же высокие основания верить в их существование» (из работы Гёделя «Russell's, Mathematical Logic» в книге The Philosophy of Bertrand Russei. Evanston; Chicago, 1944. C. 137). (Данная здесь авторами характеристика «платонизма» довольно-таки поверхностна, а традииионная квалификаиия Гёделя как платониста далеко не бесспорна. Впрочем, тема эта далеко выходит за рамки настоящей книги. См., например: Френкель А., Бар-Хиллел И. Основания теории множеств / Пер. с англ. М.: Мир, 1966. Гл. X. § 8; 3-е изд. М.: URSS, 2010. Прим. перев.)