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