Основные квазиматричные логики
Гуманитарный вестник
# 10·2016 9
Почти очевидное доказательство этого случая, а также других
случаев и их сочетаний опускается.
Лемма доказана.
Доказательство метатеоремы 2.
Поскольку формула
F
является
общезначимой, то для любого набора гипотез
B
1
, …,
B
n
для нее верно
B
1
, …,
B
n
⇒
□
F
,
или же
B
1
, …,
B
n
⇒
F
&◊¬
F
. Отсюда
B
1
, …,
B
n
⇒
F
.
Остается показать, как удалить гипотезы:
1)
B
1
, …,
B
n – 1
, □
α
n
⇒
D
;
2)
B
1
, …,
B
n – 1
,
¬◊α
n
⇒
D
;
3)
B
1
, …,
B
n – 1
,
α
n
&◊¬α
n
⇒
D
;
4)
B
1
, …,
B
n – 1
,
¬α
n
&◊α
n
⇒
D
.
Отсюда:
5)
B
1
, …,
B
n – 1
,
α
n
,
¬◊¬α
n
⇒
D
(из 1);
6)
B
1
, …,
B
n – 1
,
¬α
n
,
¬◊α
n
⇒
D
(из 2);
7)
B
1
, …,
B
n – 1
,
α
n
,
◊¬α
n
⇒
D
(из 3);
8)
B
1
, …,
B
n – 1
,
¬α
n
,
◊α
n
⇒
D
(из 4).
Далее:
9)
B
1
, …,
B
n – 1
,
α
n
⇒
D
(из 5, 7);
10)
B
1
, …,
B
n – 1
,
¬α
n
,
⇒
D
(из 6, 8);
11)
B
1
, …,
B
n – 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.