Чтобы показать, что доказуемость ~ G влечет доказуемость G, требуется аналогичное, но несколько более громоздкое рассуждение, которое мы не будем пытаться здесь воспроизводить.
Как мы уже отмечали, если и некоторая формула, и ее отрицание выводимы из некоторой системы аксиом, то эта система противоречива (несовместна). Поэтому если аксиомы формализованной системы арифметики совместимы, то ни G, ни ее отрицание не могут быть доказуемыми. Иначе говоря, если наши аксиомы непротиворечивы, то G формально неразрешима в том точном смысле, что ни G, ни ~ G не выводимы из арифметических аксиом.
3. Важность предыдущего заключения не сразу бросается в глаза. Что особенного — можно было бы задать вопрос — в том, что некоторая формула, сформулированная на арифметическом языке, оказалась неразрешимой? Но приходится признать, что из этого результата действительно вытекают чрезвычайно важные выводы. Все дело в том, что, хотя формула G и является недоказуемой, можно, как выясняется, чисто метаматематическим рассуждением установить ее истинность. Иными словами, удается показать, что формула G выражает некоторое (довольно-таки громоздко выражаемое, но тем не менее вполне определенное) свойство, с необходимостью принадлежащее всем натуральным числам (аналогично, скажем, свойству, выражаемому гораздо более простой формулой «∀ x ~ (x + 3 = 2)», интерпретируемой обычно как утверждение, что никакое натуральное число, сложенное с числом 3, не дает в сумме 2).
Приведем здесь рассуждение, устанавливающее истинность формулы G. Во-первых, в предположении непротиворечивости арифметики можно доказать, что метаматематическое утверждение
«формула „∀ x ~ Dem(x, sub(n, 13, n))“ недоказуема»
истинно. Во-вторых, такое утверждение представляется (выражается) в арифметике той самой формулой, которая в нем упоминается. В-третьих, мы вспоминаем, что истинным метаматическим утверждениям при осуществляемом посредством гёделевской нумерации отображении их в арифметику соответствуют истинные же арифметические формулы. (Именно это обстоятельство обусловливает всю плодотворность такого отображения; ситуация здесь совершенно та же, что в аналитической геометрии, где координатное «кодирование» обеспечивает перевод истинных геометрических высказываний в истинные алгебраические высказывания.) Отсюда и вытекает, что формула G, соответствующая истинному метаматематическому высказыванию, сама должна быть истинной. Следует, однако, еще раз подчеркнуть, что истинность арифметического высказывания установлена нами отнюдь не формальным выводом выражающей его формулы из аксиом, а посредством некоторого метаматематического рассуждения.
4. Теперь нам придется напомнить читателю понятие «полноты», введенное нами в заключение раздела, посвященного исчислению высказываний. Мы назвали тогда систему аксиом полной, если любое истинное предложение, выражаемое на языке данной системы, можно из них вывести. В противном случае (т. е. если не каждое истинное предложение, выразимое в данной системе, выводится из ее аксиом) система аксиом «неполна». Но мы только что как раз и установили, что G есть истинная арифметическая формула, не выводимая из арифметических аксиом, иными словами, система аксиом арифметики неполна (разумеется, в предположении непротиворечивости этой системы аксиом), более того, формальная арифметика существенно неполна: даже если добавить к ней формулу G в качестве новой аксиомы, расширенная система аксиом будет все равно недостаточна для формального вывода всех арифметических истин. Дело в том, что по отношению к пополненной таким образом системе аксиом мы можем провести в точности то же рассуждение, что и раньше, и та же конструкция даст нам новый пример предложения, истинного в расширенной арифметической системе, но не выводимого из ее аксиом, и такое предложение будет снова выражаться неразрешимой арифметической формулой. И этот поистине удивительный вывод остается в силе независимо от того, сколько раз мы ни производили бы такое расширение системы. Таким образом, мы вынуждены признать некоторую принципиальную ограниченность возможностей аксиоматического метода. Вопреки, казалось бы, самым естественным ожиданиям, запас арифметических истин оказывается столь обширным, что ни из никакой точно зафиксированной системы аксиом не удается их все формально вывести.
5. Мы подошли теперь к месту, которое можно назвать кодой это поразительной интеллектуальной симфонии — творения Гёделя. Описанные выше шаги позволили обосновать метаматематическое утверждение «если арифметика непротиворечива, то она неполна». Но Гёделю удалось доказать и нечто большее, а именно, что само условное метаматематическое утверждение (именно все утверждение в целом) изображается в формализованной арифметике некоторой доказуемой формулой.
Построить такую замечательную формулу нам будет теперь совсем нетрудно. Мы уже говорили выше (в разделе 5), что метаматематическое высказывание «арифметика непротиворечива» эквивалентно высказыванию «существует хода бы одна недоказуемая арифметическая формула». Последнее же высказывание, очевидно, представляемся в формальном (арифметическом) исчислении следующей формулой:
Ǝ y ∀ x ~ Dem(x, y). (А)
Формула эта, если выразить ее словесно, гласит: «существует по крайней мере одно натуральное число у, такое что для любого натурального x числа x и у не находятся между собой в отношении Dem». Если же интерпретировать формулу как метаматематическое высказывание, то мы получим: «существует по крайней мере одна арифметическая формула, для которой никакая последовательность формул не является ее доказательством». Таким образом, формула А как раз и представляет посылку метаматематического утверждения «Если арифметика непротиворечива, то она неполна». В то же время заключение утверждения «Она (т. е. арифметика) неполна» непосредственно вытекает из высказывания «имеется истинное арифметическое утверждение, не являющееся формально доказуемым в арифметике»; последнее же высказывание представляется в арифметическом исчислении посредством нашей старой знакомой — формулы G. Итак, условное метаматематическое высказывание «Если арифметика непротиворечива, то она неполна» представимо формулой
Ǝ у ∀ x ~ Dem(x, y) ﬤ ∀ x ~ Dem(x, sub(n, 13, n)),
которую можно было бы теперь сокращенно обозначить через «A ﬤ G». Именно для этой формулы можно установить ее формальную доказуемость, но мы не будем здесь пытаться это делать.
Покажем лишь, что формула А недоказуема. Допустим противное. Тогда, поскольку формула A ﬤ G доказуема, modus ponens позволяет нам заключить, что доказуемой должна бы быть и формула G. Но если наше исчисление непротиворечиво, G формально неразрешима, а потому, конечно, недоказуема. Таким образом, если арифметика непротиворечива, то формула А недоказуема.
Что это означает? Формула А представляет метаматематическое высказывание «Арифметика непротиворечива». Значит, если бы высказывание можно было обосновать каким нибудь рассуждением, отобразимым в последовательность формул, являющуюся доказательством в арифметическом исчислении, сама формула А была бы доказуема. Но это, как мы только что видели, невозможно, если во всяком случае считать, что арифметика непротиворечива. Мы дошли, наконец, до заключительного аккорда: нам приходится согласиться, что если арифметика непротиворечива, то непротиворечивость ее не может быть установлена никаким метаматематическим рассуждением, допускающим представление в арифметическом формализме