Исчисление высказываний

Оказывается множество тавтологий логики высказываний можно описать в рамках простой формальной аксиоматической теории - исчисления высказываний.

Определим исчисление высказываний следующим образом:

1. Символы исчисления высказываний: Ø, É, (,) и буквы X_i с целыми положительными числами в качестве индексов: X₁, X₂,…. Символы Ø и É - логические символы, символы X₁, X₂,… - переменные.

2. Формулы исчисления высказываний: а) все переменные X_i - формулы; б) если A и B - формулы, то (ØA) и (AÉB) тоже формулы.

Пример 5.1. Последовательность символов ØX₁ÉX₂ÉX₁ - выражение, но не формула.

Пример 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 называются схемами аксиом, поскольку каждое из них порождает бесконечное множество формул, являющихся аксиомами исчисления высказываний. Например, формула X₁É(X₂ÉX₁) есть аксиома, полученная по схеме 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.

Доказательство. Пусть A₁, A₂,..., A_n - вывод формулы A из G, где A_n совпадает с A. Пусть B₁, B₂,..., B_m - вывод формулы AÉB из G, где B_n совпадает с AÉB. Тогда A₁, A₂,..., A_n, B₁, B₂,..., B_m, B - вывод формулы B из G. Последняя формула в этом выводе получена применением правила modus ponens к формулам A_n и B_m.

Наша цель показать, что формула исчисления высказываний является тавтологией тогда и только тогда, когда она есть теорема. В одну сторону это совсем просто.