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
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 .