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

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

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

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

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

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

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)].

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

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

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

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

((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) Искомому свойству должны удовлетворять не все формулы, которые можно построить с помощью правил образования данной системы. Мы должны уметь показать, что по крайней мере одна формула системы этим свойством не обладает.

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