First Order Modal Logic

This chapter is constituted by two parts. The ¯rst part comprising Sections 1-5 was written by Torben Brauner and the second part comprising Sections 6-11 was written by Silvio Ghilardi. In the first part of the chapter, we give an introduction to first-order modal logic. We present a selection of logics involving constant domains, increasing domains, and varying domains, and moreover, we present a ¯rst-order intensional logic as well as a ¯rst-order version of hybrid logic. One criteria for selecting particular logics has been the availability of sound and complete proof procedures, typically axiom systems and/or tableau systems. We have compared the first-order modal logics under consideration to fragments of sorted first-order logic via appropriate versions of the standard translation. In the second part of the chapter, we review both positive and negative results con- cerning fragment decidability, Kripke completeness and axiomatizability. Modal hyperdoctrines are then introduced, as a unifying tool for analyzing the alternative semantics proposed in the literature. These alternative semantics range from specific semantics for non-classical logics (like metaframes), to interpretations in well-established mathematical frameworks (like topological spaces and toposes). Finally, the strict relationship between toplogical semantics and D. Lewis' counterpart semantics is closely investigated and an axiomatization is presented.