Логические исчисления Краткая теория
Логическая система исчисления высказываний – это аксиоматическое представление алгебры высказываний. Аксиоматическое построение теории предполагает вывод рассматриваемых в теории формул из конечного числа аксиом при помощи правил вывода. В качестве аксиом выбираются тождественно истинные формулы алгебры высказываний. Аксиоматический подход даёт возможность построения логической системы без учёта содержательной интерпретации рассматриваемых формул.
Определение 1. Понятие формулы определяется следующим образом:
-
каждая пропозициональная переменная является формулой;
-
если F, F1 и F2 – формулы, то - также являются формулами;
-
других формул нет.
В качестве аксиом выбираются следующие формулы:
где F, G, H– произвольные формулы.
Основным правилом вывода (ПВ) является правило заключения: из формулы f и формулы FG следует формула G.
Определение 2. Выводом формулы F из множества формул Г называется конечная последовательность формул B1, B2, …, Bs = F, каждая из которых является либо аксиомой, либо формулой из множества Г, либо получена из предыдущих формул этой последовательности по правилу вывода элементы множества Г называются гипотезами или посылками вывода, а формула F – выводимой из множества формул Г.
Обозначение выводимости: Г►f.
Определение3. Формула f называется доказуемой, если существует конечная последовательность формул B1, B2, …, Bs, где Bs = F, каждая из которых является либо аксиомой, либо формулой, полученной из предшествующих формул этой последовательности при помощи правила вывода. Формула F в этом случае называется теоремой, а последовательность Bi – доказательством теоремы F. Обозначения теорем: ►F.
Вывод формул и доказательство многих теорем значительно упрощается в результате применения основных теорем исчисления высказываний. Такими теоремами являются следующие теоремы.
Теорема 1 (О дедукции). Если из гипотез F1, F2, …, Fn выводится формула G, то из гипотез F1, F2, …, Fn-1 выводима формула Fn G, то есть
F1, F2, …, Fn ► G F1, F2, …, Fn-1► Fn G
Теорема 2. Для любых формул F и G следующие формулы являются теоремами исчисления высказываний:
Формулы а) и б) из теоремы 2 называются законами двойного отрицания, а формула в) – законом контрапозиции.