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

В большей части предлагаемых рассуждений я не стану проводить четкую границу между непротиворечивостью и -непротиворечивостью, однако тот вариант теоремы Гёделя, что представлен в §2.5 , по сути, гласит, что если формальная система Fнепротиворечива, то она не может быть полной, так как не может включать в себя в качестве теоремы утверждение G( F). Здесь я всего этого демонстрировать не буду (интересующиеся же могут обратиться к [ 223 ]). Вообще говоря, для того чтобы эту форму гёделевского доказательства можно было свести к доказательству в моей формулировке, система Fдолжна содержать в себе нечто большее, нежели просто «арифметику и обыкновенную логику». Необходимо, чтобы система Fбыла обширной настолько, чтобы включать в себя действия любой машины Тьюринга. Иначе говоря, среди утверждений, корректно формулируемых с помощью символов системы F, должны присутствовать утверждения типа: «Такая-то машина Тьюринга, оперируя над натуральным числом n, дает на выходе натуральное число p». Более того, имеется теорема (см. [ 223 ], главы 11 и 13), согласно которой так оно само собой и получается, если, помимо обычных арифметических операций, система Fсодержит следующую операцию (так называемую -операцию, или операцию минимизации): «найти наименьшее натуральное число, обладающее таким-то арифметическим свойством». Вспомним, что в нашем первом вычислительном примере, (A), предложенная процедура действительно позволяла отыскать наименьшеечисло, не являющееся суммой трех квадратов. То есть, вообще говоря, право на подобные вещи за вычислительными процедурами следует сохранить. С другой стороны, именно благодаря этойих особенности мы и сталкиваемся с вычислениями, которые принципиально не завершаются, — например, вычисление (В), где мы пытаемся отыскать наименьшее число, не являющееся суммой четырехквадратов, а такого числа в природе не существует.

2.9. Формальные системы и алгоритмическое доказательство

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

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

(Среди таких логических операций могут, к примеру, оказаться следующие: «если 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:

алгоритм 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» ЛОЖНО,

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

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

«ни одно предположение Pне может быть одновременно иИСТИННЫМ, иЛОЖНЫМ»,

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