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 ◻A\text{ iff }\text{for all }v\in W,(w,v)\in ̸R\text{ or }v\models A$

This can be compiled into a formula by substituting the modal formula $◻P$ by the first oder formula $\mathrm{\forall }yR(x,y)\to P^{\prime }(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
• $(\mathrm{\neg }F{)}^{*}=\mathrm{\neg }(F)$
• $(F\wedge G{)}^{*}=(F^{*}\wedge G^{*})$
• $(◻F{)}^{*}=(\mathrm{\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 $F{O}^2$.