Конструктивное определение исчисления высказываний
Алфавит и множество формул — те же (см. классические определения). Аксиомы — три конкретные формулы: A1: (a A2: ((a A3: ((┐b Правила вывода: 1. Правило подстановки: если формула В является частным случаем формулы А, то В непосредственно выводима из А. 2. Правило Modus ponens (будем обозначать МР): если набор формул A, В, С является частным случаем набора формул a, a Здесь a, a Производные правила вывода Исчисление высказываний L — это достаточно богатая формальная теория, в которой выводимы многие важные теоремы. Выводимость формул в теории L доказывается путем предъявления конкретного вывода, то есть последовательности формул, удовлетворяющих определению. 4.2. Для удобства чтения формулы последовательности вывода выписываются друг под другом в столбик, слева указываются их номера в последовательности, а справа указывается, на каком основании формула включена в вывод (то есть она является гипотезой, или получена из схемы аксиом указанной подстановкой, или получена из предшествующих формул но указанному правилу вывода и т.д.). Теорема 4.9. ├ L A Доказательство
|
(b 
