A set-theoretic translation method for (Poly)modal logics

Abstract

The paper presents a set-theoretic translation method for polymodal logics that reduces the derivability problem of a large class of propositional polymodal logics to the derivability problem of a very weak first-order set theory Ω. Unlike most existing translation methods, the one we propose applies to any normal complete finitely-axiomatizable polymodal logic, regardless if it is first-order complete. Moreover, the finite axiomatizability of Ω makes it possible to implement mechanical proof search procedures via the deduction theorem or more specialized and efficient techniques. In the last part of the paper, we briefly discuss the application of set T-resolution to support automated derivability in (a suitable extension of) Ω