Effective completeness theorems for modal logic (Q1877094)

The authors study computable model theory of modal logics. In particular, they prove that every decidable theory of modal logic has a Kripke model which is both locally decidable and globally decidable. This effective completeness theorem is proved for a number of particular first-order modal logics. For this purpose the authors develop a technique for effectively constructing Kripke models, which is analogous to well-known Henkin's method.