دانلود کتاب Algorithmic Correspondence and Completeness in Modal Logic [PhD Thesis]

This thesis takes an algorithmic perspective on the correspondence between modal and hybridlogics on the one hand, and first-order logic on the other. The canonicity of formulae, and byimplication 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 possibleare called elementary. As is well known, it is algorithmically undecidable whether a givenmodal formula defines a first-order frame condition or not. Hence, any attempt at delineatingthe 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 theclasses of Sahlqvist and inductive formulae. The approximations we consider take the formof algorithms.We develop an algorithm called SQEMA, which computes first-order frame equivalents formodal 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, andthat all formulae on which it succeeds are d-persistent (canonical), and hence axiomatizecomplete normal modal logics.