<p>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).</p>

<p>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</p>

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

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

<p>\begin{align*}
(\Box\phi)^*&amp;=\Box^-(\Box^-\bot\to\Box^+\phi^*),\\
(A\phi)^*&amp;=\Box^+\phi^*.
\end{align*}</p>

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

<p><strong>Reference:</strong></p>

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

CC BY-SA 3.0
2018-02-06T09:15:13.830Z
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
CC BY-SA 3.0
2018-02-06T09:59:58.080Z
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
CC BY-SA 3.0
2018-02-09T18:24:03.000Z
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
CC BY-SA 3.0
2018-02-09T21:22:49.250Z
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
CC BY-SA 3.0
2018-02-10T21:26:47.327Z
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
CC BY-SA 3.0
2018-02-11T10:56:59.457Z
In the presence of universal modality, you can also reduce local satisfiability to global satisfiability ($\phi$ is loc sat iff $E\phi$ is glob sat).
Emil Jeřábek
CC BY-SA 3.0
2018-02-05T21:56:38.850Z
2018-02-05T21:56:38.850Z
Emil Jeřábek
<p>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$?</p>

<p>What I know about the topic?</p>

<blockquote>
  <p>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 <a href="https://link.springer.com/article/10.1007%2Fs10849-005-5788-9" rel="noreferrer">Deciding Regular Grammar Logics with
  Converse Through First-Order Logic</a>. </p>
  
  <p>On the other hand, the ordinary $K5$ is $NP$-complete. </p>
  
  <p>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 href="https://arxiv.org/pdf/0905.3108.pdf" rel="noreferrer">A Note on the
  Complexity of the Satisfiability Problem for Graded Modal Logics</a>.
  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.</p>
</blockquote>

<cc.complexity-theory><complexity-classes><lo.logic><modal-logic>
Complexity of modal logic IK5
Bartosz Bednarczyk
# Complexity of modal logic IK5

(Asked by: username_0 on 2018-02-02)

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](https://link.springer.com/article/10.1007%2Fs10849-005-5788-9).
>
> 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](https://arxiv.org/pdf/0905.3108.pdf).
> 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.

**Tags:** cc.complexity-theory, complexity-classes, lo.logic, modal-logic

---

## 1 answers

### Answer by username_1 on 2018-02-05. Score: 4 | Accepted answer

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](https://doi.org/10.1007/3-540-58140-5_8).

> **Comments:**
> **username_0**: 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?  
> **username_1**: 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).  
> **username_0**: 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?  
> **username_1**: 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.  
> **username_0**: 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.  
> **username_1**: In the presence of universal modality, you can also reduce local satisfiability to global satisfiability ($\phi$ is loc sat iff $E\phi$ is glob sat).  

---

