{"id":544,"date":"2015-02-12T14:59:51","date_gmt":"2015-02-12T06:59:51","guid":{"rendered":"http:\/\/tsinghualogic.net\/JRC\/?p=544"},"modified":"2015-06-21T21:35:46","modified_gmt":"2015-06-21T13:35:46","slug":"talk-unified-correspondence-alessandra-palmigiano","status":"publish","type":"post","link":"http:\/\/tsinghualogic.net\/JRC\/talk-unified-correspondence-alessandra-palmigiano\/","title":{"rendered":"[talk] Unified Correspondence (Alessandra Palmigiano)"},"content":{"rendered":"

Time:<\/strong> 2015\u00a0Apr. 16 (Thu.), 10:00-11:40
\nVenue:<\/strong> Rm 3201\u00a03rd classroom-building\u00a0(\u4e09\u6559), Tsinghua University, Beijing.<\/p><\/blockquote>\n

Speaker:<\/strong> Alessandra Palmigiano<\/strong>\u00a0(Delft University of Technology)
\nTitle:\u00a0<\/strong>Unified Correspondence<\/p>\n

Abstract:<\/strong>\u00a0Sahlqvist 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.
\nSahlqvist’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.
\nIndeed, Sahlqvist theory\u00a0<\/span>has significantly broadened its scope, extending the benefits it originally imparted to classical normal modal logic to a\u00a0wide range of logics which includes, among others, intuitionistic and distributive lattice-based (normal\u00a0modal) logics [4], non-normal (regular) modal logics [12], substructural logics [5], hybrid logics [8], and\u00a0mu-calculus [1,2].
\nThe breadth of this work has stimulated many and varied applications. Some are closely related to\u00a0<\/span>the core concerns of the theory itself, such as the understanding of the relationship between different\u00a0methodologies for obtaining canonicity results [11], or of the phenomenon of pseudocorrespondence [7].
\nOther, possibly surprising applications include the dual characterizations of classes of finite lattices\u00a0<\/span>[9],\u00a0and the identifica<\/span>tion of the syntactic shape of axioms which can be translated into structural rules of a properly displayable\u00a0calculus [10]<\/span>. These and other results have given rise to a theory called unified correspondence [3].
\nAfter 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 \u00a0algorithm 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.<\/p>\n

References:<\/b><\/p>\n

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

    Time: 2015\u00a0Apr. 16 (Thu.), 10:00-11:40 Venue: Rm 3201\u00a03 […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":[],"categories":[45,10,41],"tags":[47,48],"_links":{"self":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/posts\/544"}],"collection":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/comments?post=544"}],"version-history":[{"count":4,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/posts\/544\/revisions"}],"predecessor-version":[{"id":553,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/posts\/544\/revisions\/553"}],"wp:attachment":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/media?parent=544"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/categories?post=544"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/tags?post=544"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}