### 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 |

### Fingerprint

### Keywords

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

### Cite this

*Annals of Pure and Applied Logic*,

*170*(9), 923-974. https://doi.org/10.1016/j.apal.2019.04.003

}

*Annals of Pure and Applied Logic*, vol. 170, no. 9, pp. 923-974. https://doi.org/10.1016/j.apal.2019.04.003

**Algorithmic correspondence and canonicity for non-distributive logics.** / Conradie, Willem; Palmigiano, Alessandra.

Research output: Contribution to Journal › Article › Academic › peer-review

TY - JOUR

T1 - Algorithmic correspondence and canonicity for non-distributive logics

AU - Conradie, Willem

AU - Palmigiano, Alessandra

PY - 2019/9/1

Y1 - 2019/9/1

N2 - 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.

AB - 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.

KW - Algorithmic correspondence

KW - Canonicity

KW - Modal logic

KW - Non-distributive lattices

KW - Sahlqvist correspondence

KW - Substructural logics

UR - http://www.scopus.com/inward/record.url?scp=85064956271&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85064956271&partnerID=8YFLogxK

U2 - 10.1016/j.apal.2019.04.003

DO - 10.1016/j.apal.2019.04.003

M3 - Article

VL - 170

SP - 923

EP - 974

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

SN - 0168-0072

IS - 9

ER -