4 / 11
Ю.В. Ивлев
4
Гуманитарный вестник
# 10·2016
если |
A
| =
t
c
или |
A
| =
f
c
,
то |
◊
A
|
∈
{
t
n
,
t
c
}; |
A
| =
t
n
⇒
|
◊
A
| =
t
n
; |
A
| =
f
i
⇒
|
◊
A
| =
f
i
.
Исчисление S
к
+
.
К исчислению классической логики высказыва-
ний добавляются схемы аксиом
□
A
⊃
A
; □
A
⊃
□□
A
;
◊
□
A
⊃ ◊
A
; □
A
⊃
□
◊
A
;
◊◊
A
⊃ ◊
A
;
¬
□
¬
A
⊃ ◊
A
;
◊
A
⊃ ¬
□
¬
A
;
¬◊
A
⊃
□(
A
⊃
B
); □
B
⊃
□ (
A
⊃
B
);
◊
B
⊃ ◊
(
A
⊃
B
);
◊¬
A
⊃ ◊
(
A
⊃
B
);
◊
(
A
⊃
B
)
⊃
(□
A
⊃ ◊
B
);
□(
A
⊃
B
)
⊃
(□
A
⊃
□
B
); □(
A
⊃
B
)
⊃
(
◊
A
⊃ ◊
B
)
и правило вывода (для облегчения доказательств) — замена двойного
отрицания формулы на саму формулу, и наоборот. Определения до-
казательства, теоремы и вывода обычные.
Метатеорема 1.
Каждая теорема является общезначимой фор-
мулой. Доказательство опускается.
Метатеорема
2. Каждая общезначимая формула является теоре-
мой.
Сначала автор статьи обобщил метод Хенкина и доказал обоб-
щенным методом эту метатеорему. Однако обобщенный метод Хен-
кина не решает проблему разрешимости исчисления, что не позволя-
ет использовать квазиматричную логику при проектировании и ис-
пользовании автоматических устройств. Здесь автор предлагает
другой разработанный им метод, решающий проблему разрешимо-
сти. Он является обобщением метода Кальмара.
Замечание.
Задачи разработать такой метод и применить его для
проектирования автоматических устройств сформулированы автором
в работе [3, с. 209].
Для доказательства метатеоремы 2 доказывается следующая
лемма.
Лемма.
Пусть
F
—
формула,
α
1
, …,
α
n
—
все различные перемен-
ные, входящие в
F
,
а
β
1
, …,
β
n
—
значения этих переменных. Пусть
B
i
есть
□
α
i
,
α
i
&◊¬α
i
,
¬◊α
i
или
¬α
i
&◊α
i
в зависимости от того, что
есть
β
i
:
t
n
,
t
c
, f
i
или
f
c
. Пусть
F
′
есть □
F
i
,
F
i
&◊¬
F
i
,
¬◊
F
i
или
¬
F
i
&◊
F
i
,
в зависимости от того, принимает ли
F
значение
t
n
,
t
c
, f
i
или
f
c
при
значениях
β
1
, …,
β
n
переменных
α
1
, …,
α
n
во всех альтернативных
интерпретациях, образованных на основе данной интерпретации пе-
ременных; пусть
F
′
есть □
F
i
∨
(
F
i
&◊¬
F
i
), □
F
i
∨¬◊
F
i
,
(
F
i
&◊¬
F
i
))
∨¬◊
F
i
,
(
□F
i
∨
(
F
i
&◊¬
F
i
))
∨¬◊
F
i
и т. д., в зависимости от того, принимает ли
формула
F
соответственно в некоторых альтернативных интерпрета-
циях, образованных на основе данной интерпретации переменных,
значение
t
n
,
а в некоторых — значение
t
c
;
в некоторых —
t
n
, а в неко-