Alternative Translation Techniques for Propositional and First-Order Modal Logics

We describe and analyze techniques, other than the standard relational/functional methods, for translating validity problems of modal logics into first-order languages. For propositional modal logics we summarize the □-as-Pow method, a complete and automatic translation into a weak set theory, and then describe an alternative method, which we call algebraic, that achieves the same full generality of □-as-Pow but is simpler and computationally more attractive. We also discuss the relationships between the two methods, showing that □-as-Pow generalizes to the first-order case. For first-order modal logics, we describe two extensions, of different degrees of generality, of □-as-Pow to logics of rigid designators and constant domains.