26. Метаматематика

Описание формальной теории должно быть дано на некотором языке, понятном как тому, кто ее описывает, так и его читателю (слушателю). До сих пор мы для этой цели пользовались обычным русским языком. Язык, на котором дается описание какой-нибудь формальной теории, принято называть метаязыком (или синтаксическим языком); этот язык употребляется для высказываний об этой теории. Формальные же символы самой формальной теории составляют в совокупности некоторый язык, который используется для высказываний внутри самой этой теории; этот язык называют ее предметным языком (или языком-объектом). Скажем, «Элементарная теория групп неразрешима» есть высказывание о теории групп, сделанное на русском языке, т. е. на метаязыке. В противоположность этому «(A)(B)(C)(A ∙ B = A ∙ C → B = с)» есть высказывание теории групп, записанное на предметном языке. Соотношение между метаязыком и предметным языком можно в некотором смысле уподобить соотношению между русским и французским языками с точки зрения человека, родным языком которого является русский и который изучает французский. Все начальные сведения и пояснения в словарях, грамматиках и т. п. учащийся воспринимает на русском языке (на метаязыке). Впоследствии же он начинает писать по-французски, т. е. строить предложения на предметном языке.

Теоремы, описывающие какие-либо свойства формальной теории, называются метатеоремами; их следует отличать от «предметных» теорем самой теории. Различение это не представляет труда, так как теоремы формальной теории записываются в символике этой теории, а метатеоремы - на метаязыке. Высказывание в предыдущем абзаце, относящееся к теории групп и сформулированное на русском языке, — метатеорема; высказывание же теории групп, записанное в терминах, = и т. п., есть теорема теории групп. Поскольку доказательство метатеорем требует некоторых логических средств, система этих средств должна быть известной тем, кому адресованы эти доказательства. Можно, конечно, формализовать метаязык — в принципе таким же образом, как мы формализовали исчисление предикатов. Но тогда нам придется пользоваться каким-то метаметаязыком, по отношению к которому встанет та же проблема, и так далее - без конца. Другая возможность, указанная Гильбертом, состоит, в двух словах, в том, что в метаязыке допускаются только бесспорные средства обычной логики: основные принципы такой логики должны быть ясными, понимаемыми без затруднений. Разумеется, такие спорные средства, как доказательство от противного или лемма Цорна (см. ниже, § 4.5), должны быть сразу же исключены. Что касается теорем существования, то их доказательства должны быть конструктивными; иными словами, для любого объекта, существование которого утверждается, должна указываться эффективная процедура его построения. Вообще, в метатеории можно использовать только «финитные» методы доказательства; это значит, что ни в одном доказательстве не допускается аргументация, апеллирующая к бесконечному множеству структурных свойств формул или же к бесконечному множеству операций над формулами. Далее, предполагается, что если, скажем, в качестве метаязыка взят русский язык, то фактически будет использоваться лишь некоторый очень узкий его фрагмент. (Если разрешить использовать в качестве метаязыка весь русский язык, то возникает опасность возможности вывода его средствами классических парадоксов — например, парадокса Рассела). Исследование формальных теорий, использующее логические средства, соответствующие указанным здесь ограничениям, называется метаматематикой. Говоря коротко, метаматематика — это исследование формальных теорий теми методами, которые, по общему мнению, и должны использоваться для такого рода деятельности.

Примером метаматематического понятия служит понятие непротиворечивости, рассмотренное нами в § 3.4. Данное там определение приложимо к любой формальной теории, включающей в себя исчисление высказываний. Докажем одну относящуюся к таким теориям метатеорему.

Теорема 3.7. Пусть T - формальная теория, включающая в себя исчисление высказываний. Тогда T непротиворечива в том и только в том случае, когда не каждая формула теории T является теоремой.

Доказательство. Предположим, что T противоречива и что А есть такая формула теории T, что как |— А, так и |— ~A. Вспомним, что А → (~А → В) есть теорема при любой формуле В, так как это тавтология. Таким образом, В, т. е. произвольная формула, оказывается теоремой (доказывается двукратным применением modus ponens). Чтобы доказать обратное утверждение, допустим, что любая формула теории T есть теорема. Тогда, какова бы ни была формула А из T, и сама А и ~А - теоремы. Следовательно, в этом случае T противоречива.

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

Теорема 3.8. Исчисление высказываний непротиворечиво.

Доказательство. Пусть А - теорема исчисления высказываний. Тогда А есть тавтология, ~ А не является тавтологией и, следовательно, ~A не есть теорема.

В точности такая же цепь рассуждений дает нам доказательство непротиворечивости исчисления предикатов. Однако для исчисления предикатов такое доказательство не будет принадлежать метаматематике, так как оценочная процедура, на которую опирается теорема 3.5, не является эффективной. Но непротиворечивость исчисления предикатов можно доказать и метаматематически, исходя из того обстоятельства, что оценочная процедура для фиксированной конечной области является эффективной, так как для предикатных букв и предметных переменных в конечной области существует лишь конечное количество приписываний. Не приводя здесь этого доказательства, сформулируем сам результат.

Теорема 3.9. Исчисление предикатов непротиворечиво.

Следующее метаматематическое понятие — полнота. Напомним, что значение этого понятия заключается в достаточности запаса теорем теории для какой-либо цели. Известны две важные модификации этого понятия: одна из них заключается в «максимальной непротиворечивости», другая состоит в том, что каждая общезначимая формула есть теорема. Один из возможных способов определения понятия полноты в первом смысле это тот, который приведен в § 3.4. Мы будем называть такое понятие полноты отрицательной полнотой; таким образом, формальная аксиоматическая теория отрицательно полна, если для произвольной формулы S этой теории либо |— S, либо |— ~ S. Другая разновидность понятия полноты в смысле максимальной непротиворечивости такова: формальная теория называется абсолютно полной, если добавление к ней в качестве аксиомы любой недоказуемой в ней формулы делает систему противоречивой. Если мы условимся называть, по определению, разрешимой такую формулу S, что имеет место в точности одна из доказуемостей |— S или |— ~ S, то получится, что каждая формула непротиворечивой и отрицательно полной теории разрешима.

Исчисление высказываний не является отрицательно полным, так как ни A, ни ~ A не являются теоремами. В то же время это исчисление абсолютно полно при условии, что в определении абсолютной полноты мы под аксиомами согласимся понимать схемы аксиом. Докажем это.

Теорема 3.10. Если А есть произвольная формула исчисления высказываний, то либо А есть теорема, либо присоединение формулы А к исчислению в качестве схемы аксиом приводит к его противоречивости.

Доказательство. Пусть А - формула, не являющаяся теоремой. Докажем, что если А присоединить к системе в качестве схемы аксиом, то она станет противоречивой. Поскольку А не теорема, то она не является тавтологией. Поэтому в ее истинностной таблице найдется такая строка, в которой стоит значение F. Фиксируем какую-либо одну такую строку. Подставляя теперь вместо входящих в А простых формул, принимающих для этой выбранной строки значение Т, формулу A ~A, а вместо простых формул, принимающих значение F, формулу A ~ A, мы получим некоторую формулу В, которую и возьмем в качестве аксиомы. Очевидно, что В будет всегда принимать значение F. Значит, ~ В есть тавтология, а потому - теорема. Итак, обе формулы — В и ~ В — являются теоремами в полученном расширении системы.

Исчисление высказываний полно в том смысле, что каждая общезначимая его формула является теоремой; именно это утверждение составляет содержание теоремы 3.3, причем доказательство ее принадлежит метаматематике. Аналогичное утверждение справедливо и для исчисления предикатов (гёделевская теорема о полноте), но доказательство его уже не принадлежит метаматематике. Исчисление предикатов не является ни отрицательно полным, ни абсолютно полным. Оба эти утверждения могут быть доказаны метаматематически.

Чтобы подойти к определению еще одного (на сей раз последнего - в этом изложении) метаматематического понятия, нам понадобится вспомнить описанное в § 3.5 понятие эффективной процедуры. Говоря

Кратко, эффективная процедура (или разрешающая процедура) — это метод, который можно описать как выдачу, по мере продвижения вперед, в конечное число шагов, ответов «да» или «нет» на каждый из некоторого определенного класса вопросов. Проблема нахождения разрешающей процедуры для данного класса вопросов называется проблемой разрешения этого класса. Для понятия доказательства в формальной аксиоматической теории мы потребовали существование разрешающей процедуры; но для понятия доказуемости мы этого требования не выставляли. В отличие от вопроса, является ли данная последовательность формул доказательством (решаемого исследованием рассматриваемого конечного объекта), для ответа на вопрос, является ли данная формула теоремой, приходится производить рассмотрения, выходящие за пределы данного объекта. Кроме того, в определении понятия доказательства не накладывается никаких ограничений на длину доказательства, так что исследование всех возможных доказательств, без каких-либо ограничений на их длины, не является процедурой, которая давала бы ответ на вопрос о доказуемости в конечное число шагов в случае, когда данная формула теоремой не является. В силу указанных обстоятельств для формальных теорий приобретает особое значение проблема разрешения для доказуемости, которую часто и называют просто «проблемой разрешения данной теории». Теория, проблема разрешения которой решается в положительную сторону, называется разрешимой, в противном случае теория называется неразрешимой. Примером разрешимой теории является исчисление высказываний: поскольку формула исчисления высказываний является теоремой тогда и только тогда, когда она — тавтология, метод истинностных таблиц дает эффективную процедуру разрешения. Исчисление предикатов - пример неразрешимой теории; ниже мы вернемся еще к этому вопросу.

Теперь мы коснемся вопроса о роли метаматематики в исследовании мира. Отметим прежде всего, что открытие того, что в наивной теории множеств можно получить противоречия (иными словами, обнаружение противоречивости этой теории), произвело на многих математиков совершенно ошеломляющее впечатление. Это открытие побудило математиков к попыткам спасения теории множеств, и одной из таких попыток явилось предпринятое Э. Цермело построение теории множеств в виде формальной аксиоматической теории. Другая позиция была провозглашена Расселом и Уайтхедом в Principia Mathematica. Формальная теория множеств Цермело с последующими видоизменениями и усовершенствованиями оказывается полноценной основой для построения той теории множеств, которая нужна для известной нам математики, причем в этой аксиоматической теории удается избежать появления классических теоретико-множественных парадоксов - их нельзя вывести из аксиом этой формальной теории. В то же время ее непротиворечивость не была доказана. Проблема непротиворечивости такой теории есть по существу проблема непротиворечивости классической математики — в Principia Mathematica было показано (косвенным образом), что в рамках такой теории можно построить всю классическую математику. Человеком, посягнувшим на проблему доказательства непротиворечивости классической математики, стал Давид Гильберт. Он поставил себе целью сформулировать классическую математику в виде некоторой формальной аксиоматической теории, после чего попытаться получить прямое решение проблемы непротиворечивости. Поскольку посредством построения конечных моделей нельзя было рассчитывать решить эту проблему, Гильберт предложил вместо этого использовать конечные (финитные) методы доказательства. Точнее говоря, он провозгласил в качестве допустимых методов как раз то, что мы в начале этого параграфа охарактеризовали как метаматематику. Целью Гильберта, если говорить более подробно, было построить такую формальную аксиоматическую теорию, которая была бы адекватной формализацией для построения существовавшей тогда математики, была бы, далее, непротиворечивой и, наконец, была бы полной в том смысле, что каждая формула этой теории была бы в принципе разрешимой (т. е. чтобы либо она сама, либо ее отрицание являлось теоремой). В §3.4 мы уже отмечали, что проблема непротиворечивости значительной части классической математики может быть сведена к проблеме непротиворечивости арифметики натуральных чисел (или, короче, просто арифметики) — в виде теории, основанной на аксиомах Пеано, или же в виде теории множеств, достаточно сильной для вывода в ней пеановских аксиом. После некоторых частичных успехов гильбертовской школы в доказательстве непротиворечивости арифметики надежды на получение желаемого результата были разбиты результатом, полученным в 1931 году Гёделем. Этот результат утверждает невозможность доказательства непротиворечивости формальной теории, включающей формальную арифметику, конструктивными методами, «формализуемыми в рамках самой этой теории». Чтобы охарактеризовать такого рода методы, достаточно сказать, что к ним относятся все логические принципы, принятые в метаматематике. Таким образом, метаматематическое доказательство непротиворечивости арифметики или классического анализа оказывается невозможным.

Этот замечательный результат является следствием еще более поразительной теоремы, также доказанной Гёделем. Значение последней теоремы (называемой обычно теоремой Гёделя о неполноте) исключительно велико — она показала невыполнимость программы Гильберта в ее полном виде, так как утверждает, по существу, что любая непротиворечивая формальная теория, формализующая арифметику натуральных чисел, не полна. Основную роль в доказательстве этой теоремы играет некоторое арифметическое высказывание S, обладающее тем свойством, что ни S, ни ~ S не являются теоремами, что и доказывает отрицательную неполноту теории. Поскольку S и ~ S суть именно высказывания (а не просто некоторые формулы), то — если интерпретировать их как высказывания содержательной арифметики — одно из них истинно, а другое ложно. А так как ни одно из них не доказуемо, то получается, что в арифметике имеется истинное, но не доказуемое высказывание. Иными словами, в арифметике имеется неразрешимое высказывание.

Можно было бы подумать, что этот недостаток-неполноту теории, являющейся формализацией арифметики натуральных чисел, — можно устранить, попросту присоединив к такой теории в качестве аксиомы одно из высказываний S или ~ S, где S — неразрешимое высказывание. Но Гёдель доказал, что всякая теория, являющаяся формализацией арифметики, непременно должна содержать неразрешимые высказывания. После присоединения к такой теории неразрешимого высказывания в качестве аксиомы расширенная теория по-прежнему является формализацией арифметики, и в ней по-прежнему имеются неразрешимые высказывания.

В заключение упомянем о второй из важнейших теорем метаматематики, а именно о теореме, доказанной в 1936 году американским логиком Алонзо Чёрчем. Эта теорема утверждает отсутствие эффективной процедуры для решения вопроса относительно произвольной формулы формальной теории, содержащей арифметику натуральных чисел, является ли эта формула теоремой. Эта теорема, являющаяся примером «теорем о невозможности», подобна по существу теореме о невозможности трисекции произвольного угла с помощью циркуля и линейки. Однако от обычных теорем о невозможности теорема Чёрча отличается совершенно фундаментальным образом: необходимой предпосылкой доказательства Чёрча является выдвигаемое им точное определение понятия эффективной процедуры, претендующее на то, чтобы охватить все мыслимые виды вычислительных процедур, несмотря на довольно расплывчатый интуитивный смысл этого понятия. (Между прочим, утверждение, что чёрчевское точное определение понятия эффективной процедуры действительно охватывает содержание этого понятия, известно под именем тезиса Чёрча). Гёделевская теорема 1931 года легко следует из теоремы Чёрча. С помощью теоремы Чёрча нетрудно показать и неразрешимость исчисления предикатов. После 1936 года другими математиками была доказана неразрешимость большого числа алгебраических теорий; это относится, в частности, к упоминаемым в этой книге элементарной теории групп и теории структур.

[1] И здесь (ср. со сноской на стр. 15) слово «форма» является переводом авторского «formula»; термин «формула» появится начиная с § 2.7.— Прим. ред.

[2] N может быть равно и 1 — тогда речь идет об одноместных предикатаx (свойствах), определенных для элементов множества Х. — Прим. перев.

< Предыдущая