Unified correspondence and canonicity

Correspondence theory originally arises as the study of the relation between modal formulas and first-order formulas interpreted over Kripke frames. We say that a modal formula and a first-order formula correspond to each other if they are valid on the same class of Kripke frames. Canonicity theory is closely related to correspondence theory. We say that a modal formula is canonical if it is valid on its canonical frame, or equivalently,if its validity is preserved from a modal algebra to its canonical extension, or from a descriptive general frame to its underlying Kripke frame. Canonicity is closely related to completeness. If a modal formula is canonical, then the normal modal logic axiomatized by this modal formula is complete with respect to the class of Kripke frames defined by it.
In the development of correspondence theory, the algorithmic aspect receives increasing attention. The Sahlqvist-van Benthem theorem provides an algorithm to transform a class of modal formulas, which are later called Sahlqvist formulas, into their corresponding first-order formulas. The algorithm SQEMA provides a modal language-based algorithm to transform a modal formula into a pure modal formula in an expanded language, and then translate the pure modal formula into the first-order language. SQEMA succeeds on a strictly larger class of modal formulas, which are called inductive formulas.
In recent years, unified correspondence theory is developed based on duality-theoretic and order-algebraic insights. In this approach, a very general syntactic definition of Sahlqvist and inductive formulas is given, which applies uniformly to each logical signature and is given purely in terms of the order-theoretic properties of the algebraic interpretations of the logical connectives. In addition, the Ackermann lemma based algorithm ALBA, which is a generalization of SQEMA based on order-theoretic and algebraic insights, is given, which effectively computes first-order correspondents of input formulas/inequalities, and is guaranteed to succeed on the Sahlqvist and inductive classes of formulas/inequalities.
This dissertation belong to the line of research of unified correspondence theory.
Chapter 3 applies the unified correspondence methodology to possibility semantics, and gives alternative proofs of Sahlqvist-type correspondence results to the ones in [196], and extends these results from Sahlqvist formulas to the strictly larger class of inductive formulas, and from the full possibility frames to filter-descriptive possibility frames. Chapter 4 applies the unified correspondence methodology to modal compact Hausdorff spaces, and gives alternative proofs of canonicity-type preservation results to the ones in [14]. Chapter 5 examines the power and limits of the translation method in obtaining correspondence and canonicity results. Chapter 6 is about an application of unified correspondence theory to the proof theory of strict implication logics, showing the usefulness of unified correspondence theory in the design of analytic Gentzen sequent calculi, especially when it comes to computing the corresponding analytic rules of a given sequent.