Algorithmic correspondence and canonicity for non-distributive logics

Willem Conradie*, Alessandra Palmigiano

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review


We extend the theory of unified correspondence to a broad class of logics with algebraic semantics given by varieties of normal lattice expansions (LEs), also known as ‘lattices with operators’. Specifically, we introduce a syntactic definition of the class of Sahlqvist formulas and inequalities which applies uniformly to each LE-signature and is given purely in terms of the order-theoretic properties of the algebraic interpretations of the logical connectives. We also introduce the algorithm ALBA, parametric in each LE-setting, which effectively computes first-order correspondents of LE-inequalities, and is guaranteed to succeed on a wide class of inequalities (the so-called inductive inequalities) which significantly extend the Sahlqvist class. Further, we show that every inequality on which ALBA succeeds is canonical. Projecting these results on specific signatures yields state-of-the-art correspondence and canonicity theory for many well known modal expansions of classical and intuitionistic logic and for substructural logics, from classical poly-modal logics to (bi-)intuitionistic modal logics to the Lambek calculus and its extensions, the Lambek-Grishin calculus, orthologic, the logic of (not necessarily distributive) De Morgan lattices, and the multiplicative-additive fragment of linear logic.

Original languageEnglish
Pages (from-to)923-974
Number of pages52
JournalAnnals of Pure and Applied Logic
Issue number9
Publication statusPublished - 1 Sep 2019
Externally publishedYes


  • Algorithmic correspondence
  • Canonicity
  • Modal logic
  • Non-distributive lattices
  • Sahlqvist correspondence
  • Substructural logics


Dive into the research topics of 'Algorithmic correspondence and canonicity for non-distributive logics'. Together they form a unique fingerprint.

Cite this