Abstract

This paper is an attempt at providing a systematic presentation of Quantified Modal Logics . We present a set of modular, uniform, normalizing, sound and complete labelled sequent calculi for all QMLs whose frame properties can be expressed as a finite set of first-order sentences with equality. We first present CQK, a calculus for the logic QK, and then we extend it to any such logic QL. Each calculus, called CQL, is modular , uniform , normalizing and Kripke-sound and complete for QL. We improve on the existing literature on the subject by extending the class of logics for which such a presentation is given, and by giving a new proof of soundness and completeness