2 / 8
Ю.В. Ивлев
2
Гуманитарный вестник
# 11·2017
Исчисление включает все схемы аксиом классического исчисле-
ния высказываний (КИВ), в которых метасимволы
A
,
B
,
C
обознача-
ют модализированные формулы, т. е. формулы, в которых каждая
пропозициональная переменная находится в области действия како-
го-либо из модальных терминов □ и
, modus ponens, правила Геделя
(|–A
⇒
|–□A), а также схемы аксиом:
□
A
A
;
A
□
A
;
A
A
;
A
A
;
□
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
);
□(
A
&
B
)
(□
A
&
□
B
);
(□
A
&
□
B
)
□(
A
&
B
);
(
A
&
□
B
)
(
A
&
B
);
(□
A
&
B
)
(
A
&
B
);
(
A
&
B
)
(
A
&
B
);
□
A
(
A
&
A
)
A
;
(□
A
□
B
)
□(
A
□
B
);
(
A
B
)
(
A
B
);
□(
A
B
)
(□
A
B
);
□(
A
B
)
(
A
□
B
);
(
A
B
)
(
A
B
).
Некоторые особенности исчисления
S
г
.
Во-первых, в нем имеет
место правило Геделя.
Во-вторых, все производные правила вывода классического ис-
числения высказываний, являясь правилами вывода данного исчис-
ления, применимы в выводе лишь к модализированным формулам.
Некоторые (по крайней мере некоторые) прямые правила вывода
натурального исчисления высказываний применимы и к немодализи-
рованным формулам, например правило
A
B
,
A
⇒
B
. Такие непря-
мые правила, как правило дедукции
,
⇒
⇒ ⊃
Г A B
Г А B
и сведения к абсурду
,
; ,
,
⇒ ⇒ ¬
⇒ ¬
Г A B Г A B
Г А
неприменимы к немодализированным формулам в выводе. Однако
для любых формул в выводе является действующим
ослабленное
правило сведения к абсурду
,
; ,
⇒ ⇒ ¬
⇒ ◊¬
Г A B Г A B
Г А
.
Интерпретации. Теория модальностей.
Символы □,
,
,
, &,
интерпретируются как логические термины, определяемые следую-
щими таблицами.