Modal deduction in second-order logic and set theory. I

We investigate modal deduction through translation into standard logic and set theory. In a previous paper, using a set-theoretic translation method, we proved that derivability in the minimal modal logic Ks corresponds precisely to derivability in a weak, computationally attractive set theory Ω. In this paper, this approach is shown equivalent to working with standard first-order translations of modal formulae in a theory of general frames. The employed techniques are mainly model-theoretic and set-theoretic, and they admit extensions to richer languages and modal deductive systems than that of basic modal logic. Some of these extensions are discussed in the last part of the paper.