Teopeмa Гёделя

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

Правила образования указывают, какие именно комбинации элементарных символов алфавита мы будем считать формулами нашего исчисления. Прежде всего формулой, по определению, является каждая пропозициональная переменная. Далее, если «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.