1 A General Proof of Kripke-completeness for Quantified Modal Logics

In the present paper I aim at providing a general framework to prove Kripke-completeness for normal calculi of Quantified Modal Logic. I shall consider Kripke semantics- as presented in [5]- and extensions of normal propositional modal sys-tems, based both on Kripke’s theory of quantification ([11]) and on free and classical first-order logic ([8], [9]). In [5] Corsi highlights the lack of “a common completeness proof that can cover constant domains, varying domains, and models meeting other conditions”1, on the other hand the need of such a proof has always been felt2. She attempts to provide a unified completeness theorem for Quantified Modal Logics- as the title of her paper states- for normal QML calculi based on Kripke’s theory of quantification and classical first-order logic. In the end she leaves as open problems the completeness proof for system Q◦.K + BF (on Kripke’s theory of quantification, with BF) and for system Q◦.B (on Kripke’s theory of quantification, with modal base B). The present paper- corresponding to chapter 1 in [1]- aims at extending and completing Corsi’s programme. I present a general proof of Kripke-completenes