Каждая из приведенных аксиом представляется довольно-таки «очевидной» и тривиальной.
Если, конечно, иметь в виду некоторые «естественные переводы» (т. е. интерпретации!) аксиом, самих по себе никакого «смысла» не имеющих. Аналогичное замечание следует иметь в виду при чтении следующей фразы текста и всюду в аналогичных случаях далее. — Прим. перев.
Тем не менее из них с помощью сформулированных выше двух правил преобразования можно вывести бесконечное множество теорем, многие из которых трудно назвать очевидными или тривиальными. К числу таких теорем относится, скажем, формула
((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 или K2. Формулы, не являющиеся элементарными, относятся к тому или иному из этих классов в силу следующих соглашений:
1) формула, имеющая вид S1 ˅ S2, принадлежит классу K2, если как S1, так и S2 принадлежат K2; в противном случае она принадлежит K1;
2) формула, имеющая вид S1 ﬤ S2, принадлежит классу K2, если S1 принадлежит K1, a S2 принадлежит K2; в противном случае она принадлежит K1;