Logic for Computer Scientists/Modal Logic/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:
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
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 .