Оказывается множество тавтологий логики высказываний можно описать в рамках простой формальной аксиоматической теории - исчисления высказываний.
Определим исчисление высказываний следующим образом:
1. Символы исчисления высказываний: Ø, É, (, ) и буквы Xi с целыми положительными числами в качестве индексов: X1, X2,…. Символы Ø и É - логические символы, символы X1, X2,… - переменные.
2. Формулы исчисления высказываний: а) все переменные Xi - формулы; б) если A и B - формулы, то (ØA) и (AÉB) тоже формулы.
Пример 5.1. Последовательность символов ØX1ÉX2ÉX1 - выражение, но не формула.
Пример 5.2. Пусть A, B, C - формулы. Тогда (CÉ(AÉB)), (((ØA)ÉB)É(ØC)) тоже формулы.
Для сокращения записи опустим в формуле внешние скобки и те пары скобок, без которых можно восстановить формулы по следующему правилу: каждое вхождение знака Ø относится к наикратчайшей подформуле, следующей за этим знаком. Тогда две предыдущие формулы примут вид
CÉ(AÉB), (ØAÉB)ÉØC.
Аксиомы исчисления высказываний. Каковы бы ни были формулы A, B и C, следующие формулы являются аксиомами:
A1. AÉ(BÉA);
A2. (AÉ(BÉC))É((AÉB)É(AÉC));
A3. (ØBÉØA)É((ØBÉA)ÉB).
Выражения A1-A3 называются схемами аксиом, поскольку каждое из них порождает бесконечное множество формул, являющихся аксиомами исчисления высказываний. Например, формула X1É(X2ÉX1) есть аксиома, полученная по схеме A1, формула (ØAÉØA)É((ØAÉA)ÉA) (где A - любая формула) - аксиома полученная по схеме A3.
Единственным правилом вывода формулы служит правило modus ponens (правило отделения, утверждающий модус). Пусть имеется три формулы: A, AÉB и B. Про формулу B будем говорить, что она получается по правилу modus ponens из формул A и AÉB. Формально, это правило вывода записывается в виде: A, AÉB Þ B.
Хотя для исчисления высказываний мы выбрали только два логических символа Ø и É, с помощью подходящих определений можно ввести и остальные операции Ú, &, ~, например, A~B означает Ø((BÉA)ÉØ(AÉB)).
Пример 5.3. Для любой формулы A построим вывод формулы AÉA, т. е. AÉA - теорема.
Подставляем в схему аксиом A2 вместо B формулу AÉA и вместо C формулу A, получаем аксиому
(AÉ((AÉA)ÉA))É((AÉ(AÉA))É(AÉA)). (1)
Подставляем в A1 вместо формулы B формулу AÉA, получаем аксиому
AÉ((AÉA)ÉA). (2)
Из формул (1) и (2) по правилу modus ponens получаем
(AÉ(AÉA))É(AÉA). (3)
Подставляем в A1 вместо формулы B формулу A, получаем аксиому
AÉ(AÉA). (4)
Из формул (3) и (4) по правилу modus ponens получаем AÉA.
Теорема 5.1. Если G|―AÉB и G|―A, то G|―B.
Доказательство. Пусть A1, A2,..., An - вывод формулы A из G, где An совпадает с A. Пусть B1, B2,..., Bm - вывод формулы AÉB из G, где Bn совпадает с AÉB. Тогда A1, A2,..., An, B1, B2,..., Bm, B - вывод формулы B из G. Последняя формула в этом выводе получена применением правила modus ponens к формулам An и Bm.
Наша цель показать, что формула исчисления высказываний является тавтологией тогда и только тогда, когда она есть теорема. В одну сторону это совсем просто.