[talk] Unified Correspondence (Alessandra Palmigiano)

Time: 2015 Apr. 16 (Thu.), 10:00-11:40
Venue: Rm 3201 3rd classroom-building (三教), Tsinghua University, Beijing.

Speaker: Alessandra Palmigiano (Delft University of Technology)
Title: Unified Correspondence

Abstract: Sahlqvist correspondence theory is among the most celebrated and useful results of the classical theory of modal logic, and one of the hallmarks of its success. Traditionally developed in a model-theoretic setting [13], it provides an algorithmic, syntactic identification of a class of modal formulas whose associated normal modal logics are strongly complete with respect to elementary (i.e. first-order definable) classes of frames.
Sahlqvist’s results can equivalently be reformulated algebraically, via the well known duality between Kripke frames and complete atomic Boolean algebras with operators (BAOs). This perspective immediately suggests generalizations of Sahlqvist’s theorem along algebraic lines, e.g. to the cases of distributive or arbitrary lattices with operators.
Indeed, Sahlqvist theory has significantly broadened its scope, extending the benefits it originally imparted to classical normal modal logic to a wide range of logics which includes, among others, intuitionistic and distributive lattice-based (normal modal) logics [4], non-normal (regular) modal logics [12], substructural logics [5], hybrid logics [8], and mu-calculus [1,2].
The breadth of this work has stimulated many and varied applications. Some are closely related to the core concerns of the theory itself, such as the understanding of the relationship between different methodologies for obtaining canonicity results [11], or of the phenomenon of pseudocorrespondence [7].
Other, possibly surprising applications include the dual characterizations of classes of finite lattices [9], and the identification of the syntactic shape of axioms which can be translated into structural rules of a properly displayable calculus [10]. These and other results have given rise to a theory called unified correspondence [3].
After having briefly discussed the duality between complete atomic BAOs and Kripke frames, we illustrate, by way of examples, the algebraic mechanisms underlying Sahlqvist correspondence for classical modal logic [6]. We show how these mechanisms work in much greater generality than the classical setting in which Sahlqvist theory was originally developed. Next, we present the  algorithm ALBA [4] designed to effectively calculate the first order correspondent of input formulas, thanks to which the existing most general results on correspondence can be achieved. Finally, we give an overview of the current applications and extensions of this theory.


  1. W. Conradie and A. Craig. Canonicity results for mu-calculi: an algorithmic approach. Journal of Logic and Computation, forthcoming.
  2. W. Conradie, Y. Fomatati, A. Palmigiano, and S. Sourabh. Algorithmic correspondence for intuitionistic modal mu-calculus. Theoretical Computer Science, 564:30-62, 2015.
  3. W. Conradie, S. Ghilardi, and A. Palmigiano. Unified correspondence. In A. Baltag and S. Smets, editors, Johan F.A.K. van Benthem on Logical and Informational Dynamics, volume 5 of Outstanding Contributions to Logic, pages 933-975. Springer, 2014.
  4. W. Conradie and A. Palmigiano. Algorithmic correspondence and canonicity for distributive modal logic. Annals of Pure and Applied Logic, 163(3):338-376, 2012.
  5. W. Conradie and A. Palmigiano. Algorithmic correspondence and canonicity for non-distributive logics. Journal of Logic and Computation, forthcoming.
  6. W. Conradie, A. Palmigiano, and S. Sourabh. Algebraic modal correspondence: Sahlqvist and beyond. Submitted, 2014.
  7. W. Conradie, A. Palmigiano, S. Sourabh, and Z. Zhao. Canonicity and relativized canonicity via pseudo-correspondence: an application of ALBA. Submitted, 2014.
  8. W. Conradie and C. Robinson. On Sahlqvist theory for hybrid logic. Journal of Logic and Computation, forthcoming.
  9. S. Frittella, A. Palmigiano, and L. Santocanale. Dual characterizations for finite lattices via correspondencetheory for monotone modal logic. Journal of Logic and Computation, forthcoming.
  10. G. Greco, M. Ma, A. Palmigiano, A. Tzimoulis, and Z. Zhao. Unified correspondence as a proof-theoretic tool. Submitted, 2015.
  11. A. Palmigiano, S. Sourabh, and Z. Zhao. J?onsson-style canonicity for ALBA-inequalities.  Journal of Logic and Computation, forthcoming.
  12. A. Palmigiano, S. Sourabh, and Z. Zhao. Sahlvist theory for impossible worlds. Journal of Logic and Computation, forthcoming.
  13. H. Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logic. In Studies in Logic and the Foundations of Mathematics, volume 82, pages 110-143. 1975.