Действительно, перечисленные связки возникли как сокращенные обозначения для указанных в скобках выражений; более того, при устном чтении формул исчисления высказываний этими выражениями часто называют соответствующие формальные символы (скажем, формула «~ p q» читается как «не p или q» и т. п.). Следует, однако, твердо помнить, что эти «названия» связок не нужны для описания исчисления (неинтерпретированного!) как такового; они относятся к его метатеории, и, скажем, электронно-вычислительная машина, производящая операции с формулами исчисления высказываний как с таковыми, в такого рода «названиях» не нуждается. — Прим. перев.
Правила образования указывают, какие именно комбинации элементарных символов алфавита мы будем считать формулами нашего исчисления. Прежде всего формулой, по определению, является каждая пропозициональная переменная. Далее, если «S» обозначает некоторую формулу[2], то ее «формальное отрицание» «~ (S)» также есть формула. Аналогично, если «S1» и «S2»суть обозначения некоторых формул, то выражения «(S1) (S2)», «(S1) (S2)» и «(S1)·(S2)» также суть формулы.
Примеры формул:
«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). Согласно этому правилу из любых двух формул, имеющих соответственно вид «S1» и «S1 S2», можно вывести и формулу «S2». Например, из формул «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.
