Как же первоначальное кенигсбергское доказательство Гёделя связано с тем, что я представил в §2.5? Не будем углубляться в детали, укажем лишь на наиболее существенные моменты. В роли формальной системы Fиз исходной теоремы Гёделя выступает наша алгоритмическая процедура A:

Роль же представленного Гёделем в Кенигсберге предположения G( F), которое в действительности утверждает непротиворечивость системы F, играет полученное в §2.5конкретное предположение «вычисление  C _k( k) не завершается», недоказуемое посредством процедуры A, но интуитивно представляющееся истинным, коль скоро процедуру А мы полагаем обоснованной:

Возможно, такая замена позволит лучше понять, каким образом убежденность в обоснованности процедуры — такой, например, как  A— может привести к другой процедуре, с исходной никак не связанной, но в обоснованности которой мы такжедолжны быть убеждены, поскольку если мы полагаем процедуры некоторой формальной системы Fобоснованными — т.е. процедурами, с помощью которых мы получаем одни лишь действительные математические истины, полностью исключив ложные утверждения (иными словами, если некое предположение  P выводится из такой процедуры как ИСТИННОЕ, то это значит, что оно и в самом деле должно быть истинным), — то мы должны также уверовать и в ω-непротиворечивость системы F. Если под «ИСТИННЫМ» понимать «истинное», а под «ЛОЖНЫМ» — «ложное» (как оно, собственно, и есть в рамках любой обоснованной формальной системы F), то безусловно истинно следующее утверждение:

что в точности совпадает с условием ω-непротиворечивости.

Однако убежденность в ω-непротиворечивости формальной системы Fможет происходить не только из убежденности в обоснованности этой системы, но и из убежденности в ее обыкновенной непротиворечивости. Поскольку если под «ИСТИННЫМ» понимать «истинное», а под «ЛОЖНЫМ» — «ложное», то, несомненно, выполняется условие

в точности совпадающее с условием непротиворечивости. Вообще говоря, во многих случаях различия между непротиворечивостью и ω-непротиворечивостью практически отсутствуют. Для упрощения дальнейших рассуждений этой главы я, в общем случае, не стану разделять эти два типа непротиворечивости и буду обычно говорить просто о «непротиворечивости». Суть доказательства Гёделя и Россера сводится к тому, что установление факта непротиворечивости формальной системы (достаточно обширной) превышает возможности этой самой формальной системы. Первоначальный (кенигсбергский) вариант теоремы Гёделя опирался только на ω-непротиворечивость, однако следующий, более известный, вывод был связан уже исключительно с непротиворечивостью обыкновенной.

Сущность гёделевского доказательства в нашем случае состоит в том, что оно показывает, как выйти за рамки любого заданного набора вычислительных правил, полагаемых обоснованными, и получить некое дополнительное правило, в исходном наборе отсутствующее, но которое также должно полагать обоснованным, — т.е. правило, утверждающее  непротиворечивостьисходных правил. Важно уяснить следующий существенный момент:

Мы имеем право применять правила формальной системы Fи полагать, что выводимые из нее результаты действительно  истинны, только в том случае, если мы также полагаем, что эта формальная система непротиворечива. (Например, если бы система Fне была непротиворечивой, то мы могли бы вывести, как ИСТИННОЕ, утверждение «1 = 2», которое истинным, разумеется, не является!) Таким образом, если мы уверены, что применение правил некоторой формальной системы Fдействительно эквивалентно математическому рассуждению, то следует быть готовым принять и рассуждение, выходящее за рамки системы F, какой бы эта система F ни была.

Продолжим рассмотрение различных математических возражений, высказываемых время от времени в отношении моей трактовки доказательства Гёделя—Тьюринга. Многие из них тесно связаны друг с другом, однако я полагаю, что в любом случае их будет полезно разъяснить по отдельности.

Что касается формальной системы F, описывающей общую теорию множеств, то, действительно, не всегда ясно, можно ли вообще говорить о каком-то абсолютном смысле, в котором то или иное утверждение о множествах является либо «истинным», либо «ложным», — вследствие чего под сомнение может попасть и само понятие «обоснованности» формальной системы, подобной F. В качестве поясняющего примера приведем один известный результат, полученный Гёделем (1940) и Коэном (1966). Они показали, что определенные математические утверждения (так называемые континуум-гипотезаКантора и аксиома выбора) никак не зависят от теоретико-множественных аксиом системы Цермело—Френкеля— стандартной формальной системы, обозначаемой здесь через ZF. (Аксиома выбора гласит, что для любой совокупности непустых множеств существует еще одно множество, которое содержит ровно один элемент из каждого множества совокупности ^{29} . Согласно же континуум-гипотезе Кантора, количество подмножеств натуральных чисел — равное количеству вещественныхчисел — представляет собой вторую по величине бесконечность после множества собственно натуральных чисел ^{30} . Читателю нет нужды вникать в скрытый смысл этих утверждений прямо сейчас. Равно как нет нужды и мне углубляться в подробное изложение аксиом и правил процедуры системы ZF.) Некоторые математики убеждены в том, что система ZFохватывает все методы математического рассуждения, необходимые для обычной математики. Некоторые даже утверждают, будто приемлемым математическим доказательством можно считать только такое доказательство, какое можно, в принципе, сформулировать и доказать в рамках системы ZF. (См. комментарий к возражению Q14, где дается оценка применимости к таким субъектам гёделевского доказательства.) Иными словами, эти математики настаивают на том, что ИСТИННЫМИ, ЛОЖНЫМИ и НЕРАЗРЕШИМЫМИ в рамках системы ZFматематическими утверждениями можно считать только те утверждения, истинность, ложность и неразрешимость которых, в принципе, устанавливается математическими средствами. Для таких людей аксиома выбора и континуум-гипотеза являются математически неразрешимыми (что, по их мнению, и доказывается выводом Гёделя—Коэна), и они наверняка будут утверждать, что истинность или ложность этих двух математических утверждений суть предметы достаточно условные.