Строго позитивные фрагменты модальных логик с направленностью

Доклад основывается на недавно вышедшей статье A. Kudinov, S. Kikot. On Strictly Positive Fragments of Modal Logics with Confluence. Mathematics. 2022. Vol. 10. No. 19. https://www.mdpi.com/2227-7390/10/19/3701
Строго позитивный фрагмент модальной логики – это множество формул вида $A \to B$, где $A$ и $B$ формулы, составленные с помощью констант $\top$ и $\bot$, переменных, модальности "возможно" и конъюнкции. Такие формулы называют строго позитивными импликациями. Строго позитивные фрагменты изучаются в различных контекстах, включая логику доказуемости и дескрипционную логику. Обычно строго позитивный фрагмент обладает хорошими свойствами, например, сравнительно низкой вычислительной сложностью.
Мы рассматривали логики содержащие аксиому направленности: $\mathbf{A2} = \Diamond \Box p \to \Box \Diamond p$. Мы нашли строго позитивные фрагменты логик $\mathbf{K.2} = \mathbf{K} + \mathbf{A2}, \mathbf{D2}, \mathbf{D4.2}, \mathbf{S4.2}$.
Аксиома направленности не является строго позитивной импликацией, поэтому ее нужно заменить на ее строго позитивный эквивалент. Мы показали, что таким эквивалентом является формула $\Diamond \top \to \Diamond \Diamond \top$. Причем в случае, когда исходная логика сериальна (т.е. содержит формулу $\Diamond \top$), то добавление аксиомы направленности не меняет строго позитивный фрагмент логики.
Кроме этого, мы изучали произведения модальных логик. Произведение должно содержать двухмодальный вариант аксиомы направленности, который часто называют аксиомой Чёрча-Россера: $\Diamond_1 \Box_2 p \to \Box_2 \Diamond_1 p$. Оказалось, что в этом случае ситуация сильно отличается. Мы показали, что чтобы аксиоматизировать логику, содержащую аксиому Чёрча-Россера, нужно добавить бесконечно много формул специального вида. Но если исходные логики сериальны, то добавление этих формул не требуется.