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

В предложенной мною формулировке доказательства Гёделя—Тьюринга (см. §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 как ИСТИННЫЕ, были бы тождественны всем тем вычислениям, незавершаемость которых определяется с помощью процедуры А.

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

алгоритм А <—> правила системы F.

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

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

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

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

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

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

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

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

убежденность в обоснованности равносильна убежденности в непротиворечивости.

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

2.10. Возможные формальные возражения против (продолжение)

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