# 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:

${\displaystyle 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 ${\displaystyle \square P}$ by the first oder formula ${\displaystyle \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 ${\displaystyle F}$ we define its translation ${\displaystyle F^{*}}$:

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

As a result we have

## Theorem 1

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

Together with the observation that validity in modal logic ${\displaystyle 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 ${\displaystyle FO^{2}}$.