Логика булевых функций

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

В соответствии с общими принципами построения формальных систем (исчислений) исчисление высказываний определяется следующим образом.

1 Символы исчисления высказываний включают в себя: а) знаки логических операций , б) буквы X_i с целыми положительными индексами i; в) скобки и запятую – ( , ).
2. Формулами исчисления высказываний являются:
а) все переменные X_i;
б) если A и B – формулы, то A – формула и A  B – формула.
Хотя для исчисления высказываний выбраны только два логических символа и  и только два типа формул A и A  B, можно с помощью следующих известных равносильностей ввести и другие логические символы и формулы:
A & B  A  B);
A  B  A  B;
A  B  (( A B)  ( B  A )).
3. Аксиомы исчисления высказываний. Существуют различные системы аксиом исчисления высказываний, обладающие свойствами непротиворечивости, независимости и полноты. Будем использовать следующую систему аксиом:
А1. A  (B  A);
А2. (A  (B  C))  ((A  B)  (A  C));
А3. (B  A)  ((B  A) B).
Непосредственной проверкой можно убедиться, что аксиомы есть тождественно-истинные формулы. Например, для аксиомы А1:
A  (B  A)A  B  A  И.
4. Правило вывода в исчислении высказываний одно – modus ponens (m. p.) – правило заключения:
, или A, AB ├ B.
Аксиомы исчисления высказываний являются формулами. Аксиомы и формулы можно рассматривать как схемы, так что любую входящую в них переменную можно заменять формулами.
Пример 3.1.
Если в правиле modus ponens переменную B заменить формулой A&B, получим правило вывода
.
Всякую выведенную в исчислении высказываний формулу можно рассматривать как правило вывода, которое может быть присоединено к уже имеющимся правилам.
Вывод формулы представляет собой последовательность формул, сопровождаемых указаниями, является ли данная формула гипотезой, аксиомой или получена из других формул по некоторому правилу вывода. Принято вначале выписать все гипотезы и слева указывать номер шага вывода.
Пример 3.2.
Построим вывод формулы A ├ B A.
(1) A – гипотеза;
(2) A (B A) – аксиома А1;
(3) B A – из (1) и (2) по m. p.
Очевидно, что любую равносильную формулу можно рассматривать как правило вывода. Например, закон де Моргана может быть представлен как следующее правило вывода: . Равносильность A B B  A порождает закон контрапозиции: .
С учетом сказанного перечислим правила вывода исчисления высказываний.
1. Введение конъюнкции: .
2. Удаление конъюнкции: и .
3. Отрицание конъюнкции: .
4. Введение дизъюнкции: и .
5. Удаление дизъюнкции: и .
6. Отрицание дизъюнкции: .
7. Введение импликации: .
8. Удаление импликации: (m. p.) и .
9. Отрицание импликации: .
10. Введение эквивалентности: .
11. Удаление эквивалентности: и .
12. Введение отрицания: .
13. Удаление отрицания: .
14. Закон контрапозиции: .
Для построения выводов в исчислении высказываний полезной оказывается следующая теорема.