Тени разума. В поисках науки о сознании

Поставив перед собой задачу построить на основе процедуры 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:

алгоритм A ↔ правила системы F.

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

утверждение «вычисление C_k(k) не завершается» ↔ утверждение «система F непротиворечива».

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

не все предположения P(0), P(1), P(2), P(3), P(4), … могут быть ИСТИННЫМИ, если утверждение «предположение P(n) справедливо для всех натуральных чисел n» ЛОЖНО,