Algorithmic correspondence and canonicity for non-distributive logics

Willem Conradie, Alessandra Palmigiano

Research output: Contribution to JournalArticleAcademicpeer-review

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 languageEnglish
Pages (from-to)923-974
Number of pages52
JournalAnnals of Pure and Applied Logic
Volume170
Issue number9
DOIs
Publication statusPublished - 1 Sep 2019
Externally publishedYes

Fingerprint

Correspondence
Logic
Lambek Calculus
Intuitionistic Logic
Modal Logic
Signature
Substructural Logics
Algebraic Semantics
Linear Logic
Classical Logic
Multiplicative
Fragment
First-order
Class
Operator

Keywords

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

Cite this

@article{85c14332c1474bd4a9c749ceb9bb6f2f,
title = "Algorithmic correspondence and canonicity for non-distributive logics",
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.",
keywords = "Algorithmic correspondence, Canonicity, Modal logic, Non-distributive lattices, Sahlqvist correspondence, Substructural logics",
author = "Willem Conradie and Alessandra Palmigiano",
year = "2019",
month = "9",
day = "1",
doi = "10.1016/j.apal.2019.04.003",
language = "English",
volume = "170",
pages = "923--974",
journal = "Annals of Pure and Applied Logic",
issn = "0168-0072",
publisher = "Elsevier",
number = "9",

}

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

In: Annals of Pure and Applied Logic, Vol. 170, No. 9, 01.09.2019, p. 923-974.

Research output: Contribution to JournalArticleAcademicpeer-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 -