Математическая логика и теория алгоритмов. Стенюшкина В.А. - 30 стр.

         9 Свойства исчисления высказываний

         9.1 Полнота

        Имеют место следующие метатеоремы.
        Теорема 9.1 Всякая теорема исчисления высказываний есть тавтология.
        Теорема 9.2 Всякая тавтология является теоремой исчисления высказыва-
ний .
      Таким образом, теоремами теории L являются тождества - истинные фор-
мулы и только они. А это означает, что формальная теория L, то есть классиче-
ское исчисления высказываний, является полной.

         9.2 Непротиворечивость

      Из теоремы 9.1 следует, что теория L непротиворечива. Действительно.
Любая теорема в L есть тавтология. Отрицание тавтологии не есть тавтология,
то есть в L нет одновременной выводимости теоремы и ее отрицания, что соот-
ветствует определению непротиворечивости формальной теории.

         9.3 Разрешимость

      Теория L разрешима как формальная теория. Алгоритм, который опреде-
ляет для любой формулы теории, является ли эта формула теоремой теории,
может состоять в вычислении истинностных значений формулы в каждой инте-
рпретации. Принципиально это выполнимо за конечное время в силу конечнос-
ти числа интерпретаций и числа операций, присутствующих в формуле.

         9.4 Исследование системы аксиом ИВ. Независимость

     Подмножество α множества всех аксиом данной ФТ называется незави-
симым, если ни одна из формул α не может быть выведена с помощью правил
вывода из аксиом, не входящих в α.
     Известно, что каждая из схем аксиом А1, А2, А3 независима. Эта система
аксиом предложена П.С. Новиковым; она весьма проста, но существует много
других систем, работающих тоже хорошо.
     Примеры
     1 Гильберт, Аккерман, 1938:
     - связки: ∨,  ;
     - аксиомы: А∨А → А; А → А∨В; А∨В → В∨А, (В → С) → (А∨В → А∨С);
     -правило: Modus Ponens.
     2 Россер, 1953:
     - связки:∨,  ;
     - аксиомы: А → А ∧ А; А → А ∧ В → А; (А → В) → ( ( В∧ С) → (С∧ А);
     -правило: Modus Ponens.