# Complexity of modal logic IK5

What is the complexity of local satisfiability problem for modal logic $\mathit{IK5}$? Herein we denote by $IK5$ the modal logic over euclidean frames extended with inverse modality. Could you provide any references? Is it in $NP$?

What I know about the topic?

It's easy to see that $IK5$ is in $ExpTime$, since there is a reduction from it to $GF^2$ (the two-variable guarded fragment of first-order logic) - see Deciding Regular Grammar Logics with Converse Through First-Order Logic.

On the other hand, the ordinary $K5$ is $NP$-complete.

We can write an equisatisfiable formula in $FO^1$ (the one-variable fragment of first-order logic), because the models can be devided into three parts: (1) starting world $w$, (2) sucessors of $w$ (3) sucessors of sucessors of $w$. The example reduction for even harder logic ($K5$ with graded modalities) is described in A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics. However in the presence of inverse modality we cannot do the same trick - the brief idea is that inverse worlds could require the different number of successors.

The logic is EXP-complete. One way to prove the lower bound is to note that the logic KTB augmented with universal modality, or even just the global consequence relation of KTB, is EXP-complete (Chen and Lin [1]; note that they denote KTB as B).

Note that a connected IK5-frame $(W,R,R^{-1})$ is either a single irreflexive point, or it consists of a reflexive cluster $C$ together with a (possibly empty) set $I$ of irreflexive points, each of which sees (in $R$) a nonempty subset of $C$. Thus, $$R_s:=\{(x,y)\in C^2:\exists z\in I\,(R(z,x)\land R(z,y))\}$$ is a symmetric relation on $C$; if every element of $C$ is seen by an element of $I$, $R_s$ is also reflexive. Conversely, it is easy to see that every reflexive symmetric frame can be obtained in this way. It follows that

$${}\vdash_{\mathrm{KTB}^U}\phi\iff{}\vdash_{\mathrm{IK5}}\Diamond^-\top\land\Box^+\Diamond^-\Box^-\bot\to\phi^*,$$

where the translation $\phi^*$ commutes with propositional connectives, and is defined for modal operators by

\begin{align*} (\Box\phi)^*&=\Box^-(\Box^-\bot\to\Box^+\phi^*),\\ (A\phi)^*&=\Box^+\phi^*. \end{align*}

Here, $A$ denotes the universal modality of $\mathrm{KTB}^U$, and $\Box^+$ and $\Box^-$ respectively denote the forward and backward modalities of IK5.

Reference:

[1] Cheng-Chia Chen and I-Peng Lin, The complexity of propositional modal theories and the complexity of consistency of propositional modal theories, in: Proc. LFCS 1994 (Anil Nerode and Yu. V. Matiyasevich, eds.), LNCS 813, Springer, pp. 69–80, doi 10.1007/3-540-58140-5_8.

• Maybe a silly question. As far I as I understand, you proved that global consequence in IK5 is at least as hard as global consequence in KTB^U. Since local satisfiability is a special case of global consequence problem, how we get hardness for it? – Bartosz Bednarczyk Feb 6 '18 at 9:15
• No, I proved that theoremhood (which is a special case of both local and global consequence) in IK5 is at least as hard as theoremhood in KTB^U. Or dually, satisfiability in IK5 is as hard as satisfiability in KTB^U. Having said that, it does not really make any difference: local consequence and theoremhood have the same complexity in any modal logic by the deduction theorem, and local and global consequence have the same complexity in any logic with a definable universal modality (which IK5 has). – Emil Jeřábek Feb 6 '18 at 9:59
• Emil Jeřábek, are you aware of any upper bound results for IK5? Different techniques then translating into GF2, which I mentioned in my post? – Bartosz Bednarczyk Feb 9 '18 at 18:24
• A fairly easy filtration argument shows that any satisfiable formula has model of size $2^{O(n)}$, which means one can test satisfiability in NEXP. I don't know a direct way how to make the algorithm deterministic. – Emil Jeřábek Feb 9 '18 at 21:22
• The last question. Could you tell me if that result gives us also any bound on global satisfiability problem (I'm not familiar with theoremhood, that's why I'm asking)? It's easy to reduce global satisfiability to local satisfiability if you can use universal modality, but maybe upper bound for IK5 is smaller than Exp. – Bartosz Bednarczyk Feb 10 '18 at 21:26