Эрнст Нагель - Teopeма Гёделя

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 формально неразрешима, а потому, конечно, недоказуема. Таким образом, если арифметика непротиворечива, то формула А недоказуема.

Что это означает? Формула А представляет метаматематическое высказывание «Арифметика непротиворечива». Значит, если бы высказывание можно было обосновать каким нибудь рассуждением, отобразимым в последовательность формул, являющуюся доказательством в арифметическом исчислении, сама формула А была бы доказуема. Но это, как мы только что видели, невозможно, если во всяком случае считать, что арифметика непротиворечива. Мы дошли, наконец, до заключительного аккорда: нам приходится согласиться, что если арифметика непротиворечива, то непротиворечивость ее не может быть установлена никаким метаматематическим рассуждением, допускающим представление в арифметическом формализме

Надо сказать, что этот замечательный результат проведенного Гёделем анализа проблемы не исключает, однако, возможности метаматематического доказательства непротиворечивости арифметики. Из него следует лишь, что невозможно такое доказательство непротиворечивости, которое могло бы быть отображено (переведено) в формальное доказательство, проводимое внутри самой формальной арифметики.

Положение здесь очень напоминает то, которое сложилось в геометрии в связи о доказательством невозможности деления произвольного угла на три части о помощью циркуля и линейки. Доказательство это отнюдь не исключает возможности произвести искомое деление при помощи каких-либо более сильных средств. И действительно, его можно осуществить, добавив к циркулю и линейке ещё постоянный эталон длины.

На самом деле метаматематические доказательства непротиворечивости арифметики были получены; первым такое доказательство осуществил представитель школы Гильберта Герхард Генцен в 1936 г., а впоследствии было получено еще несколько доказательств того же результата. Доказательства эти имеют большую логическую ценность, заключающуюся хотя бы уже в том, что они продемонстрировали существенно новые формы метаматематических рассуждений и конструкций, а также в том, что благодаря им выяснилось, какие новые виды правил вывода надо допустить, если мы хотим установить непротиворечивость арифметики. Но все подобные доказательства уже не могут быть воспроизведены в рамках арифметического исчисления, и, поскольку все новые правила вывода уже не являются финитистскими, доказательства непротиворечивости, полученные с их помощью, никоим образом нельзя считать достижением цели, поставленной в гильбертовской программе в ее первоначальной формулировке.