Logic for Computer Scientists/Modal Logic/Translation Method

Translation Method

There are several methods aiming at a translation of propositional modal logics into first order predicate logics. The idea is, to transform the semantic conditions for the reachability into logical formulae: One rule for the definition of the semantic was:

$w \models \Box A \;\; \mbox{ iff } \mbox{for all } v \in W, (w,v)\not\in R \mbox{ or } v\models A$

This can be compiled into a formula by substituting the modal formula $\square P$ by the first oder formula $\forall y R(x,y) \to P'(y)$ . Hence we can eliminate all modal operators by introducing the first order translations. The result of such a translation is a classical first order formula, which can be processed by the methods we have seen before.

For a modal formula $F$ we define its translation $F^*$:

• $P^* = P(x)$, if $P$ is a propositional constant
• $(\lnot F)^* = \lnot (F)$
• $(F \land G)^* = (F^* \land G^*)$
• $(\square F)^* = (\forall y (R(x,y) \to F^*(x/y)))$, where $y$ is a new variable not occurring in $F^*$ and $F^*(x/y)$ is the result of replacing all free occurrences of $x$ in $F^*$ by $y$.

As a result we have

Theorem 1

F is a valid modal formal in $K$ iff $F^*$ is a valid first order formula.

Together with the observation that validity in modal logic $K$ (like in many others) is decidable, we hence have a sublogic of first order classical predicate logic which is decidable! Modal logic can be seen as a fragment of 2-variable first-order logic $FO^2$.