(Среди таких логических операций могут, к примеру, оказаться следующие: «если P& Q, то P»; «если Pи P=> Q, то Q»; «если x[ P( x)], то P( n)»; «если ~ x[ P( x)], то x[~ P( x)]» и т.п. Символы «&», «=>», «», «», «~» означают здесь, соответственно, «и», «следует», «для всех [натуральных чисел]», «существует [натуральное число]», «не»; в этот ряд можно включить и некоторые другие аналогичные символы.)

Поставив перед собой задачу построить на основе процедуры Eформальную систему E, мы можем начать с некоторой в высшей степени фундаментальной (и, со всей очевидностью, непротиворечивой) формальной системы L, в рамках которой выражаются лишь вышеупомянутые простейшие правила логического вывода, — например, с так называемого исчисления предикатов(см. [ 223 ]), которое только на это и способно, — и построить систему Eпосредством присоединения к системе Lпроцедуры Eв виде дополнительных аксиом и правил процедуры для L, переведя тем самым всякое высказывание P, получаемое из процедуры E, в разряд ИСТИННЫХ. Это, впрочем, вовсе не обязательно окажется легко достижимым на практике. Если процедура Eзадается всего лишь в виде спецификации машины Тьюринга, то нам, возможно, придется присоединить к системе L(как часть ее алфавита и правил процедуры) все необходимые обозначения и операции машины Тьюринга, преждечем мы сможем присоединить саму процедуру Е в качестве, по сути, дополнительной аксиомы. (См. окончание §2.8 ; подробности в [ 223 ].)

Собственно говоря, в нашем случае не имеет большого значения, содержит ли система E, которую мы таким образом строим, ИСТИННЫЕ предположения, отличные от тех, что можно получить непосредственно из процедуры E(да и примитивные логические правила системы Lвовсе не обязательно должны являться частью заданной процедуры E). В §2.5 мы рассматривали гипотетический алгоритм A, который по определению включал в себя все процедуры (известные или познаваемые), которыми располагают математики для установления факта незавершаемости вычислений. Любому подобному алгоритму неизбежно придется, помимо всего прочего, включать в себя и все основные операции простого логического вывода. Поэтому в дальнейшем я буду подразумевать, что все эти вещи в алгоритме Aизначально присутствуют.

Следовательно, как процедуры для установления математических истин, алгоритмы (т. е. вычислительные процессы) и формальные системы для нужд моего доказательства, в сущности, эквивалентны. Таким образом, несмотря на то, что представленное в §2.5 доказательство было сформулировано исключительно для вычислений, оно сгодится и для общих формальных систем. В том доказательстве, если помните, речь шла о совокупности всех вычислениях (действий машины Тьюринга) C q( n). Следовательно, для того чтобы оно оказалось во всех отношениях применимо к формальной системе F, эта система должна быть достаточно обширной для того, чтобы включать в себя действия всех машин Тьюринга. Алгоритмическую процедуру A, предназначенную для установления факта незавершаемости некоторых вычислений, мы можем теперь добавить к правилам системы Fс тем, чтобы вычисления, предположения о незавершающемся характере которых устанавливаются в рамках Fкак ИСТИННЫЕ, были бы тождественны всем тем вычислениям, незавершаемость которых определяется с помощью процедуры A.

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

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

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

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

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

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