Effective completeness theorems for modal logic

We initiate the study of computable model theory of modal logic, by proving effective completeness theorems for a variety of first-order modal logics. We formulate a natural definition of a decidable Kripke model, and show how to construct such a decidable Kripke model of a given decidable theory. Our construction is inspired by the effective Henkin construction for classical logic. The Henkin construction, however, depends in an essential way on the Deduction Theorem. In its usual form the Deduction Theorem fails for modal logic. In our construction, the Deduction Theorem is replaced by a result about objects called finite Kripke diagrams. We argue that this result can be viewed as an analogue of the Deduction Theorem for modal logic.