Файл: Пеноуз Роджер. Тени разума. В поисках науки о сознании.doc

2.8. Условие -непротиворечивости

Наиболее известная форма теоремы Гёделя гласит, что фор­мальная система F (достаточно обширная) не может быть од­новременно полной и непротиворечивой. Это не совсем та зна­менитая «теорема о неполноте», которую Гёдель первоначаль­но представил на конференции в Кенигсберге (см. §§2.1 и 2.7), а ее несколько более сильный вариант, который был позднее получен американским логиком Дж. Баркли Россером(1936). По своей сути, первоначальный вариант теоремы Гёделя оказыва­ется эквивалентен утверждению, что система F не может быть одновременно полной и -непротиворечивой. Условие же -непротиворечивости несколько строже, нежели условие непроти­воречивости обыкновенной. Для объяснения его смысла нам по­требуется ввести некоторые новые обозначения. В систему обо­значений формальной системы F необходимо включить символы некоторых логических операций. Нам, в частности, потребуется символ, выражающий отрицание («не»); можно выбрать для этого символ «~». Таким образом, если Q есть некое высказы­вание, формулируемое в рамках F, то последовательность сим­волов ~ Q означает «не Q». Нужен также символ, означающий «для всех [натуральных чисел]» и называемый квантор общно­сти', он имеет вид «V». Если Р (п) есть некое высказывание, за­висящее от натурального числа п (т. е. Р представляет собой так называемую пропозициональную функцию), то строка симво­лов Vn [Р (п)] означает «для всех натуральных чисел п высказы­вание Р (п) справедливо». Например, если высказывание Р (п) имеет вид «число п можно выразить в виде суммы квадратов трех чисел», то запись Vn [Р (п)] означает «любое натуральное число является суммой квадратов трех чисел», — что, вообще говоря, ложно (хотя, если мы заменим «трех» на «четырех», то это же утверждение станет истинным). Такие символы можно записывать в самых различных сочетаниях; в частности, строка символов

выражает отрицание того, что высказывание Р (п) справедливо для всех натуральных чисел п.

Условие же -непротиворечивости гласит, что если выска­зывание  можно доказать с помощью методов фор­мальной системы F, то это еще не означает, что в рамках этой самой системы непременно доказуемы все утверждения

Р(0),Р(1),Р(2),Р(3),Р(4), ....

Отсюда следует, что если формальная система F не является -непротиворечивой, мы оказываемся в аномальной ситуации, ко­гда для некоторого Р оказывается доказуемой истинность всех высказываний Р(0), Р(1), Р(2), Р(3), Р(4), ...; и одновре­менно с этим можно доказать и то, что не все эти высказывания истинны! Безусловно, ни одна заслуживающая доверия формаль­ная система подобного безобразия допустить не может. Поэтому если система F является обоснованной, то она непременно будет и -непротиворечивой.

В дальнейшем утверждения «формальная система F явля­ется непротиворечивой» и «формальная система F является -непротиворечивой» я буду обозначать, соответственно, символа­ми «G (F)» и «П (F)». В сущности (если полагать систему F до­статочно обширной), сами утверждения (? (F) и П (F) формулиру­ются как операции этой системы. Согласно знаменитой теореме Гёделя о неполноте, утверждение G (F) не является теоремой системы F (т. е. его нельзя доказать с помощью процедур, допу­стимых в рамках системы F), не является теоремой и утвержде­ние fi (F) — если, разумеется, система F действительно непро­тиворечива. Несколько более строгий вариант теоремы Гёделя, сформулированный позднее Россером, гласит, что если система F непротиворечива, то утверждение ~ G (F) также не является те­оремой этой системы. В оставшейся части этой главы я буду фор­мулировать свои доводы не столько исходя из утверждения fi (F), сколько на основе более привычного нам G (F), хотя для большей части наших рассуждений в равной степени сгодится любое из них. (В некоторых наиболее явных аргументах главы 3 я буду иногда обозначать через «G(F)» конкретное утверждение «вы­числение Ck (k) не завершается» (см. §2.5); надеюсь, никто не сочтет это слишком большой вольностью с моей стороны.)

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

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

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

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

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

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

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

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