Оказывается, что к числу теорем нашего исчисления относится формула «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 или K2. Формулы, не являющиеся элементарными, относятся к тому или иному из этих классов в силу следующих соглашений:
1) формула, имеющая вид S1 ˅ S2, принадлежит классу K2, если как 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». В каждом из столбцов указаны классы, которым принадлежат соответствующие формулы при данных распределениях значений переменных по этим классам. Вот как выглядит таблица для первой аксиомы: