Критерий допустимости правил вывода логики $S5_2C_n$

Голованов М.И.


В работах \cite{wolt, vvr} показано, что строение бимодальной логики может
быть весьма сложным, даже если каждая из её модальностей удовлетворяет сильным
аксиомам. В предлагаемой работе рассматривается пропозициональная логика
$S5_2C_n$, являющаяся расширением классического исчисления
высказываний, при котором к логическим операторам ИВ добавляются два
модальных операторов $\Box_0$ и $\Box_1,$ и каждый из них удовлетворяет
аксиомам $S5$ и аксиоме $(\Box_0 \Box_1)^n p \equiv (\Box_1 \Box_0)^n p$.
Получен критерий допустимости правил вывода.
\begin{thm}\label{acss}
Правило вывода $A(p_1\dots,p_m)/B(p_1\dots,p_m)$ не допустимо в логике
$S5_2C_n$ тогда и только тогда, когда выполняются следующие условия: \newline
1) $((\Box_0\Box_1)^n A\to B)\notin S5_2C_n$, \newline
2) на одноэлементной модели существует означивание
${\cal E}$ такое, что ${\cal E}\Vdash A$.
\end{thm}
Используя теорему \ref{acss} можно построить алгоритм проверки допустимости правил
вывода для логики $S5_2C_n$. Следовательно имеем
\begin{cor}
Логика $S5_2C_n$ разрешима относительно допустимости правил вывода.
\end{cor}
\begin{thebibliography}{6}
\bibitem{wolt}
F.Wolter, What is the upper part of the lattice of bimodal logics?
Studia Logica, 53, No.2, (1994), 235--242.
\bibitem{vvr}
V.V.Rybakov, Schemes of theorems for first order theories as propositional
modal logic, Abstracts of the 1992 European Summer Meeting of ASL,
Veszpr\'{e}m, Hungary, 1992, 64.
\bibitem{mig976}
Golovanov M.I. {\sl Bimodal propositional logic $S5_2C_n$,}
{\bf Bulletin of the section of logic}, v.26, N. 3, pp. 118-125.
\end{thebibliography}