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

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