Frame correspondences in modal predicate logic

Understanding modal predicate logic is a continuing challenge, both philosophical and mathematical. In this paper, I study this system in terms of frame correspondences, finding a number of definability results using substitution methods, including new analyses of axioms in intermediate intuitionistic predicate logics. The semantic arguments often have a different flavour from those in propositional modal logic. But eventually, I hit boundaries to first-order definability of frame conditions. I then relate these findings to the known incompleteness theorems for modal predicate logic, and point out some new directions for further research, including the use of strengthened higher-order proof systems for the basic modal language.