## Abstract

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 language | English |
---|---|

Pages (from-to) | 923-974 |

Number of pages | 52 |

Journal | Annals of Pure and Applied Logic |

Volume | 170 |

Issue number | 9 |

DOIs | |

Publication status | Published - 1 Sep 2019 |

Externally published | Yes |

## Keywords

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