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:


This can be compiled into a formula by substituting the modal formula by the first oder formula . 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 we define its translation :

  • , if is a propositional constant
  • , where is a new variable not occurring in and is the result of replacing all free occurrences of in by .

As a result we have

Theorem 1[edit]

F is a valid modal formal in iff is a valid first order formula.

Together with the observation that validity in modal logic (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 .