On Kripke completeness of modal predicate logics around quantified K5.

The paper studies completeness and incompleteness of modal predicate logics in Kripke semantics, especially for logics of the form Q Λ , minimal predicate extensions of modal propositional logics. We show that Q Λ is incomplete for a continual family of logics Λ above K + □ (□ p → p) , in particular for well-known K5 and K45. On the other hand, in some cases we find completions of Q Λ ; they are obtained by adding a single extra axiom. Completeness proofs use canonical models, with some modifications, and the case of QK5 is the most interesting from the technical side. We also introduce the "boxing" operation for modal predicate logics and prove transfer results for Kripke and Kripke sheaf completeness with respect to this operation. [ABSTRACT FROM AUTHOR]