Algorithmic Correspondence and Completeness in Modal Logic [PhD Thesis]

This thesis takes an algorithmic perspective on the correspondence between modal and hybrid logics on the one hand, and first-order logic on the other. The canonicity of formulae, and by implication the completeness of logics, is simultaneously treated. Modal formulae define second-order conditions on frames which, in some cases, are equiv- alently reducible to first-order conditions. Modal formulae for which the latter is possible are called elementary. As is well known, it is algorithmically undecidable whether a given modal formula defines a first-order frame condition or not. Hence, any attempt at delineating the class of elementary modal formulae by means of a decidable criterium can only consti- tute an approximation of this class. Syntactically specified such approximations include the classes of Sahlqvist and inductive formulae. The approximations we consider take the form of algorithms. We develop an algorithm called SQEMA, which computes first-order frame equivalents for modal formulae, by first transforming them into pure formulae in a reversive hybrid language. It is shown that this algorithm subsumes the classes of Sahlqvist and inductive formulae, and that all formulae on which it succeeds are d-persistent (canonical), and hence axiomatize complete normal modal logics.