Основные квазиматричные логики

9 / 11

Основные квазиматричные логики
Гуманитарный вестник # 10·2016 9
Почти очевидное доказательство этого случая, а также других
случаев и их сочетаний опускается.
Лемма доказана.
Доказательство метатеоремы 2. Поскольку формула F является
общезначимой, то для любого набора гипотез B 1, …, Bn для нее верно
B1 , …, Bn ⇒ □F, или же B1, …, Bn ⇒ F&◊¬ F. Отсюда B 1, …, B n ⇒ F.
Остается показать, как удалить гипотезы:
1) B1, …, Bn – 1, □αn ⇒ D;
2) B1, …, Bn – 1, ¬◊αn ⇒ D ;
3) B1, …, Bn – 1, αn&◊¬αn ⇒ D ;
4) B1, …, Bn – 1, ¬αn&◊αn ⇒ D .
Отсюда:
5) B1, …, Bn – 1, αn, ¬◊¬αn ⇒ D (из 1);
6) B1, …, Bn – 1, ¬αn, ¬◊αn ⇒ D (из 2);
7) B1, …, Bn – 1, αn, ◊¬αn ⇒ D (из 3);
8) B1, …, Bn – 1, ¬αn, ◊αn ⇒ D (из 4).
Далее:
9) B1, …, Bn – 1, αn ⇒ D (из 5, 7);
10) B1 , …, Bn – 1, ¬αn, ⇒ D (из 6, 8);
11) B1 , …, Bn – 1 ⇒ D (из 9, 10) и т. д.
Метатеорема доказана.
Формализация основных квазматричных четырехзначных логик и
доказательство соответствующих метатеорем проводятся следующим
образом: проверяются на общезначимость приведенные в рассмот-
ренной выше системе схемы аксиом. Те из них, которые не являются
общезначимыми, отбрасываются. Начинается доказательство мета-
теорем о полноте. По мере потребности в новых схемах аксиом они
включаются в аксиоматику, проверяясь предварительно на общезначи-
мость. Затем, если возможно, минимизируется число схем аксиом, если
удается показать, что некоторые из них являются производными.
Во всех основных квазиматричных четырехзначных логиках
определения отрицания и импликации идентичные. Все соответству-
ющие исчисления содержат следующие схемы аксиом:
□A ⊃ A; ¬□¬A ⊃ ◊ A; ◊A ⊃ ¬□¬A; ¬◊A ⊃ □(A ⊃ B); □ B ⊃ □(A ⊃ B);
◊ B ⊃ ◊ (A ⊃ B); ◊¬A ⊃ ◊(A ⊃ B ); ◊( A ⊃ B) ⊃ (□A ⊃ ◊B).
В логике Sк
+ дополнительными схемами являются: □A ⊃ □□A;
◊ □A ⊃ ◊ A; □A ⊃ □◊ A; ◊◊A ⊃ ◊A, □(A ⊃ B) ⊃ (□A ⊃ □B);
□(A ⊃ B) ⊃ (◊ A ⊃ ◊B). В логике Sа
+ — □(A ⊃ B) ⊃ (□A ⊃ □B);
□(A ⊃ B) ⊃ (◊ A ⊃ ◊ B).
Исследование выполнено при финансовой поддержке РГНФ в
рамках научного проекта № 15-03-00372.