Конструктивное определение исчисления высказываний

Алфавит и множество формул — те же (см. классические определения). Аксиомы — три конкретные фор­мулы:

A₁: (a (b a));

A₂: ((a (b c)) ((a b) (a c)));

A₃: ((┐b ┐a) ((┐b a) b)).

Правила вывода:

1. Правило подстановки: если формула В является частным случаем формулы А, то В непосредст­венно выводима из А.

2. Правило Modus ponens (будем обозначать МР): если набор формул A, В, С является частным случаем набора формул a, a b, b, то формула С является непосредственно выводимой из формул А и В.

Здесь a, a b, b — это три конкретные формулы, построенные с помощью переменных а,b и связки ®.

Производные правила вывода

Исчисление высказываний L — это достаточно богатая формальная теория, в которой выводимы многие важные теоремы.

Выводимость формул в теории L доказывается путем предъявления конкретного вывода, то есть последовательности формул, удовлетворяющих определению. 4.2. Для удоб­ства чтения формулы последовательности вывода выписываются друг под другом в столбик, слева указываются их номера в последовательности, а справа указывается, на каком основании формула включена в вывод (то есть она является гипотезой, или получена из схемы аксиом указанной под­становкой, или получена из предшествующих формул но указанному правилу вывода и т.д.).

Теорема 4.9. _{├ L} A A

Доказательство