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 yR(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}$.