Modal Correspondence Theory
Johan van Benthem

Abstract:
Modal Correspondence Theory
Johan van Benthem

Modal Correspondence Theory has for its subject the connections between modal formulas and formulas of classical logical systems, both viewed as means of expressing relational properties. Two main questions are treated in this dissertation: which modal formulas are definable in first-order logic and which first-order formulas are definable by means of modal formulas? As for the first, it is shown that a modal formula is first-order definable if and only if it is preserved under ultrapowers. Moreover, two methods are developed, one using first-order substitutions for second-order quantifiers to show constructively that modal formulas satisfying certain syntactic conditions are first-order definable, the other using the Löwenheim-Skolem theorem to show that certain modal formulas are not first-order definable. For the case of modal reduction principles, a class of modal formulas to which most better-known modal axioms belong, these two methods yield a complete syntactic answer to the first question. As for the second question, there is a theorem by R.I. Goldblatt and S.K. Thomason about \Sigma\Delta-elementary classes of relational structures, characterizing the modally definable ones in terms of closure under four algebraic operations. A new proof of this result is given here, as well as a series of preservation results for the algebraic operations it involves. From these results it follows that a first-order formula is modally definable only if it is equivalent to a "restricted  positive" formula constructed from atomic formulas and the falsum (a constant denoting a fixed contradiction), using conjunction, disjunction and restricted quantifiers.