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

Символы, формулы, аксиомы исчисления высказываний.
Правила вывода

Рассмотрим формальную аксиоматическую систему, в некотором смысле адекватную алгебре высказываний. Назовем эту систему исчислением высказываний.

Чтобы построить исчисление, нужно определить алфавит исчисления, понятие формулы, класс формул, называемых аксиомами, правила вывода данного исчисления.

Символы исчисления высказываний состоят из знаков трех категорий:

Большие латинские буквы А, В, С, ... X, Y, Z, ..., которые назовем переменными высказываниями.

Символы операций исчисления Ù, Ú, ®, ^¾ (знак конъюнкции, дизъюнкции, следования и отрицания).

Скобки ( ).

Других символов система исчисления высказываний не содержит.

Формулой в исчислении высказываний является некоторая последовательность символов. Но не всякая последовательность символов есть формула. Например, последовательности А→В (С→) и (А В) не являются формулами. Определение формулы в исчислении высказываний задается следующим образом:

1. Всякое переменное высказывание есть формула.

2. Если a, b есть формулы, то выражения вида (aÙb), , , (aÚb), (a®b) также являются формулами.

Зададим в исчислении высказываний класс исходных истинных формул-аксиом.

I.	1.	А®(В®А);
	2.	(А® (В®С))®((А®В)®(А®С);
II.	1.	АÙВ®А;
	2.	АÙВ®В;
	3.	(А®В)®((А®С)®(А®ВÙС));
III.	1.	А®АÚВ;
	2.	В®АÚВ;
	3.	(А®С)®((В®С)(АÚВ®С)).
IV.	1.	;
	2.	;
	3.	.

Правила вывода позволяют из данной системы аксиом получать другие истинные формулы исчисления высказываний. Назовем формулу исчисления высказываний ложной, если ее отрицание истинно. Будем обозначать истинные формулы буквой R, ложные – F.

К основным правилам вывода относятся два:

1) Правило заключения.

Если a и (a®b) – истинные формулы, то b также истинна. Это предложение можно записать в виде

.

2) Правило подстановки

Пусть некоторая формула a содержит переменное высказывание А. Тогда, заменив высказывание А всюду, где оно встречается, любой формулой b, получим истинную формулу. Это предложение записывается в виде .

Формула называется выводимой в исчислении высказываний, если ее можно получить, применяя правила вывода к аксиомам исчисления высказываний. Утверждение, что формула b выводима, записывают так:

├b.

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