Logic for Computer Scientists/Modal Logic/Translation Method

From Wikibooks, open books for an open world
< Logic for Computer Scientists‎ | Modal Logic
Jump to: navigation, search

Translation Method[edit]

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[edit]

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.