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

Мы покажем здесь коротко, как можно формализовать элементарную логику высказываний, являющуюся некоторым фрагментом системы, описанной в Principia Mathematica. В результате формализации упомянутый фрагмент Principia станет исчислением, состоящим из неинтепретированных символов. После этого мы уже сможем провести нужнее нам доказательство.

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

Алфавит логики высказываний (называемой часто «пропозициональным исчислением») очень несложен. Он состоит из переменных и констант. Переменные, поскольку вместо них можно подставлять предложения (sentences) системы, называют сентенциональными (чаще — пропозициональными) переменными. В качестве переменных мы будем использовать буквы «p», «q», «r», …, «p1», «p2» …, «q1», «q2» ….

Постоянные символы (константы) — это «пропозициональные» связки и знаки препинания. Мы будем употреблять следующие пропозициональные связки: «~» читается как «не»; ˅ — «или»; «ﬤ» — «если…, то…»; «·» — «и»; знаки препинания: «(» — «левая скобка», «)» — «правая скобка».

Действительно, перечисленные связки возникли как сокращенные обозначения для указанных в скобках выражений; более того, при устном чтении формул исчисления высказываний этими выражениями часто называют соответствующие формальные символы (скажем, формула «~  p ˅  q » читается как «не p или q » и т. п.). Следует, однако, твердо помнить, что эти «названия» связок не нужны для описания исчисления (неинтерпретированного!) как такового; они относятся к его метатеории, и, скажем, электронно-вычислительная машина, производящая операции с формулами исчисления высказываний как с таковыми, в такого рода «названиях» не нуждается. — Прим. перев.

Правила образования указывают, какие именно комбинации элементарных символов алфавита мы будем считать формулами нашего исчисления. Прежде всего формулой, по определению, является каждая пропозициональная переменная. Далее, если «S» обозначает некоторую формулу, то ее «формальное отрицание» «~ (S)» также есть формула. Аналогично, если «S1» и «S2»суть обозначения некоторых формул, то выражения «(S1) ˅ (S2)», «(S1) ﬤ (S2)» и «(S1)·(S2)» также суть формулы.

Примеры формул:

«p», «~ p», «(р) ﬤ (q)», «((q) ˅ (r)) ﬤ (p)».

Однако выражения «(p)(~ q)» или «((р)ﬤ(q))˅» формулами не являются, так как они не удовлетворяют приведенному здесь определению формулы.

Правил преобразования имеется два. Первое из них — правило подстановки (вместо пропозициональных переменных) — гласит, что из произвольной формулы можно вывести другую формулу посредством одновременной подстановки некоторой формулы вместо некоторой входящей в исходную формулу пропозициональной переменной, причем такая подстановка (одна и та же) должна производиться вместо каждого вхождения выбранной переменной. Например, из формулы «p ﬤ p» можно, подставив вместо переменной «p» переменную (а тем самым — формулу) «q», вывести формулу «q ﬤ q»; подставив в ту же исходную формулу вместо «p» формулу «p ˅ q», мы выведем формулу «(p ˅ q) ﬤ (p ˅ q)» и т. п. Или, если интерпретировать «p» и «q» как некоторые русские предложения, то из «p ﬤ p» можно, например, получить предложения «Лягушки квакают ﬤ лягушки квакают», «(Летучие мыши слепы ˅ летучие мыши едят мышей) ﬤ (летучие мыши слепы ˅ летучие мыши едят мышей)» и т. п. Второе правило преобразования — это так называемое правило отделения (или modus ponens). Согласно этому правилу из любых двух формул, имеющих соответственно вид «S1» и «S1 ﬤ S2», можно вывести и формулу «S2». Например, из формул «p ˅ ~ p» и «(p ˅ ~ p) ﬤ (p ﬤ p) мы можем вывести «p ﬤ p».

Наконец, аксиомами нашего исчисления (по существу теми же, что в Principia Mathematicaявляются следующие четыре формулы;

1. (p ˅ p) ﬤ p

[если p или p, то p];

2. p ﬤ (p ˅ q)

[если p, то p или q];

3. (p ˅ q) ﬤ (q ˅ p)

[если p или q, то q или p];

4. (p ﬤ q) ﬤ ((r ˅ р) ﬤ (r ˅ q))

[если p влечет q, то (r или p) влечет (r или q)].

Здесь вначале приведены аксиомы, а в квадратных скобках указаны их «переводы» на обычный язык.

Каждая из приведенных аксиом представляется довольно-таки «очевидной» и тривиальной.

Если, конечно, иметь в виду некоторые «естественные переводы» (т. е. интерпретации!) аксиом, самих по себе никакого «смысла» не имеющих. Аналогичное замечание следует иметь в виду при чтении следующей фразы текста и всюду в аналогичных случаях далее. — Прим. перев.

Тем не менее из них с помощью сформулированных выше двух правил преобразования можно вывести бесконечное множество теорем, многие из которых трудно назвать очевидными или тривиальными. К числу таких теорем относится, скажем, формула

((p ﬤ q) ﬤ ((r ﬤ s) ﬤ t)) ﬤ ((u ﬤ ((r ﬤ s) ﬤ t)) ﬤ ((p ﬤ u) ﬤ (s ﬤ t))).

В данный момент нас, однако, не интересует вывод теорем из аксиом. Цель наша состоит в том, чтобы показать непротиворечивость этой системы аксиом, т. е. дать «абсолютное» доказательство невозможностивывода из данных аксиом с помощью правил преобразования никакой формулы S одновременно с ее формальным отрицанием ~S.

Оказывается, что к числу теорем нашего исчисления относится формула «p ﬤ (~ p ﬤ q)» (выражаемая словесно следующим образом: «если p, то не p влечет q»). (Мы примем этот результат к сведению, не проводя фактического его доказательства.) Допустим, что некоторая формула S, так же как и ее отрицание ~ S, выводима из аксиом. Подставляя тогда S вместо переменной «p» в только что упомянутую теорему (пользуясь правилом подстановки) и применяя затем дважды modus ponens, мы получим, что теоремой является и формула «q».

Подставляя  S вместо ( p ) в « p ﬤ (~  p ﬤ q)», мы получим сначала « S ﬤ (~ S ﬤ q )». Беря затем эту формулу и формулу S в качестве посылок modus ponens, получим «~  S ~ q ». Наконец, из последней формулы и ~  S также по modus ponens получим формулу « q ».

Но если формула, состоящая из одной-единственной переменной «q», является теоремой, то поскольку вместо «I» можно подставить любую формулу, то любая формула нашего исчисления оказывается выводимой из аксиом. Отсюда видно, что если какая- либо формула S вместе со своим отрицанием ~ S является теоремой рассматриваемого исчисления, то в нем теоремой является любая формула. Короче говоря, каждая формула противоречивого исчисления является теоремой — из противоречивой системы аксиом можно вывести любую формулу. Но этот же результат можно выразить и в «обратной» форме: если не каждая формула исчисления является теоремой (т. е. имеется хотя бы одна формула, не выводимая из данных аксиом), то это исчисление непротиворечиво. Таким образом, наша задача сводится к тому, чтобы показать, что имеется по крайней мере одна формула, не выводимая из рассматриваемой системы аксиом.

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

(1) Свойство это должно выполняться для всех четырех аксиом.

(2) Свойство это должно быть «наследственным» по отношению к правилам преобразования; иначе говоря, если оно присуще всем аксиомам, то оно должно принадлежать и любой формуле, выводимой из этих аксиом. А поскольку формула, выводимая из аксиом, есть, по определению, теорема, то данное условие сводится к тому, что искомым свойством должна обладать каждая теорема.

(3) Искомому свойству должны удовлетворять не все формулы, которые можно построить с помощью правил образования данной системы. Мы должны уметь показать, что по крайней мере одна формула системы этим свойством не обладает.

Если нам удастся найти свойство формул системы, удовлетворяющее перечисленным трем условиям, то задача построения абсолютного доказательства непротиворечивости системы будет решена. В самом деле, это свойство, будучи наследственным и принадлежа аксиомам, принадлежит и теоремам; значит, если некоторое знакосочетание, являясь формулой данной системы, не обладает указанным свойством, то это — не теорема. Иначе говоря, если член, подозреваемый в принадлежности некоему семейству (формула), лишен фамильных черт, присущих каждому настоящему члену семейства (идущих от общих предков — аксиом), то он на самом деле не может принадлежать этого клану (быть теоремой). Но если нам удалось найти формулу данной системы, не являющуюся теоремой, то мы тем самым доказали непротиворечивость этой системы — ведь, как мы совсем недавно отмечали, в системе, не являющейся непротиворечивой, каждая формула выводима из аксиом (т. е. каждая формула является теоремой). Короче говоря, все, что нам надо для решения нашей задачи, — это найти хоть одну формулу, не обладающую наследственным свойством, удовлетворяющим описанным выше условиям.

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

Но для того чтобы наше доказательство непротиворечивости было не относительным, а абсолютным, нам придется дать такое определение понятия тавтологии, которое не зависело бы непосредственно от понятия истины (в свою очередь, подразумевающего некоторую интерпретацию), а было бы дано в чисто формальных, структурных терминах.

Напомним, что формула нашего исчисления — либо просто одна из букв, используемых в нем в качестве пропозициональных переменных (назовем такие формулы «элементарными»), либо же составлена из таких букв с помощью пропозициональных связок и скобок. Условимся отнести каждую элементарную формулу в один из двух непересекающихся классов, в сумме дающих все множество формул исчисления — K1 или K 2 . Формулы, не являющиеся элементарными, относятся к тому или иному из этих классов в силу следующих соглашений:

1) формула, имеющая вид S1 ˅ S2, принадлежит классу K 2 , если как S1, так и S2 принадлежат K2; в противном случае она принадлежит K1;

2) формула, имеющая вид S1 ﬤ S2, принадлежит классу K2, если S1 принадлежит K1, a S2 принадлежит K2; в противном случае она принадлежит K1;

3) формула, имеющая вид S1 · S2, принадлежит классу K1, если как S1, так и S2 принадлежат K1; в противном случае она принадлежит K2;

4) формула, имеющая вид ~ S, принадлежит классу K2, если S принадлежит K1; в противном случае она принадлежит K1.

Теперь мы определяем свойство «быть тавтологией»: формула есть тавтология тогда и только тогда, когда она принадлежит классу K1 независимо от того, какому из классов K1 и K2 принадлежит любая из входящих в нее элементарных формул (т. е. переменных). Ясно, что это определение не использует никакой модели или интерпретации нашей системы. Мы можем установить, является ли какая-либо данная формула тавтологией, просто исследуя ее строение с точки зрения выполнения приведенных выше четырех условий.

Такая проверка приводит к выводу, что каждая из четырех аксиом является тавтологией. Процедура такой проверки сводится к составлению таблицы, в которой учитываются все возможные варианты соотнесения элементарных компонент данной аксиомы к любому из двух классов, K1 и K2. Просматривая последовательно строки такой таблицы, мы можем определить для каждого из возможных распределений «значений» (т. е. принадлежности классам K1 и K2) элементарных формул (т. е. попросту переменных), какому из классов принадлежит каждая неэлементарная «подформула» данной формулы и вся рассматриваемая формула в целом. Возьмем, например, первую аксиому. Таблица для нее состоит из трех столбцов: первый из них соответствует единственной ее элементарной компоненте «p», второй — неэлементарной подформуле «(p ˅ p)», а третий — всей формуле «(p ˅ p) ﬤ p». В каждом из столбцов указаны классы, которым принадлежат соответствующие формулы при данных распределениях значений переменных по этим классам. Вот как выглядит таблица для первой аксиомы:

p p˅p (p˅p)ﬤp

K1 K1 K1

K2 K2 K1

В первом столбце таблицы приведены возможные значения единственной элементарной компоненты рассматриваемой аксиомы, во втором — соответствующие значения неэлементарной компоненты аксиомы (согласно условию (1), в третьем — значения самой аксиомы (согласно условию (2)). Из последнего столбца сразу видно, что первая аксиома принадлежит классу K1 всегда, независимо от того, к какому классу отнесена ее элементарная компонента. Значит, первая аксиома является тавтологией.

А вот такая же таблица для второй аксиомы:

p q p˅q рﬤ(р˅q)

K1 K1 K1 K1

K1 K2 K1 K1

K2 K1 K1 K1

K2 K2 K2 K1

В первых двух столбцах таблицы указаны все возможные распределения двух элементарных компонент аксиомы по двум классам, в третьем — соответствующие значения ее неэлементарной компоненты (согласно условию (1)), в четвертом — значения самой аксиомы. И здесь из рассмотрения последнего столбца таблицы сразу видно, что аксиома является тавтологией. Точно так же устанавливается тавтологичность остальных двух аксиом.

Докажем теперь, что свойство «быть тавтологией» наследственно относительно применений правила modus ponens. (Доказательство его наследственности относительно правила подстановки предоставляется читателю.) Пусть формулы S1 и S1 ﬤ S2 — тавтологии; нам надо доказать, что тогда и формула S2 есть тавтология. Допустим, что S2 не является тавтологией. В таком случае для хотя бы одного распределения элементарных компонент этой формулы по классам K1 и K2 она принадлежит классу K2. Но, по предположению, S1 является тавтологией, т. е. принадлежит классу Ki при любых распределениях своих элементарных компонент, в том числе и при том, при котором S2 принадлежит K2. Но тогда при этом распределении формула S1 ﬤ S 2 должна (в силу второго условия) принадлежать классу K2, что, однако, противоречит предположению о тавтологичности S1 ﬤ S 2 . Противоречие показывает, что S2 должна быть тавтологией. Таким образом, тавтологичность формулы есть свойство наследственное, т. е. передаваемое от посылок правила modus ponens к его заключению.

Теперь нам остается указать пример формулы нашего исчисления, не являющейся тавтологией. Такова, например, формула «p ˅ q», принадлежащая классу K2, если обе ее компоненты («p» и «q») принадлежат этому классу. (В переводе на содержательный язык: высказывание «„p“ или q“» ложно, если ложны оба входящие в его состав высказывания «p» и «q».)

Наша цель достигнута. Мы нашли формулу, не являющуюся теоремой нашей системы. Но в случае противоречивости выбранной нами системы аксиом такой формулы в нашем исчислении не нашлось бы. Таким образом, из аксиом исчисления высказываний нельзя вывести никакой формулы одновременно с ее отрицанием. Этим и завершается абсолютное доказательство непротиворечивости исчисления высказываний.

Легко видеть, что классы K1 и K2 можно понимать соответственно как класс истинных и класс ложных высказываний. Мы, однако, намеренно воздерживались от этой терминологии в ходе самого доказательства (хотя не раз, комментируя отдельные ее шаги, подразумевали возможность ее использования), чтобы подчеркнуть то обстоятельство, что наше доказательство в принципе не нуждается в ссылках на какую бы то ни было интерпретацию формул исчисления высказываний, хотя понять его как следует легче именно при таком «переводе» на содержательный язык.

В заключение следует сказать еще об одной важной проблеме, относящейся к исчислению высказываний. Мы установили, что каждая теорема этого исчисления является тавтологией, т. е. — если выражаться в терминах неоднократно упоминаемой выше содержательной интерпретации — логической истиной, «законом логики». Естественно задать в известной мере и обратный вопрос: каждое ли логически истинное высказывание, выразимое на языке нашего исчисления (т. е. каждая ли тавтология), является теоремой данного исчисления (выводимой из его аксиом)? И на этот вопрос можно дать положительный ответ; но доказательство такого факта слишком длинно, чтобы приводить его здесь. Но нам хотелось бы обратить внимание на одно обстоятельство, не имеющее отношения к самому доказательству: дело в том, что результат этот свидетельствует о достаточности выбранных нами аксиом для получения всех тавтологичных формул — иными словами, всех логически истинных высказываний, выразимых на языке исчисления высказываний. Системы аксиом, обладающие таким свойством, принято называть «полными».

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

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

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