References & Citations
Mathematics > Logic
Title: Algorithmic correspondence and canonicity for non-distributive logics
(Submitted on 28 Mar 2016 (v1), last revised 4 Apr 2016 (this version, v2))
Abstract: We extend the theory of unified correspondence to a very 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 very general 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. Together with this, we introduce a variant of the algorithm ALBA, specific to the setting of LEs, 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. The projection of these results yields state-of-the-art correspondence theory for many well known substructural logics, such as the Lambek calculus and its extensions, the Lambek-Grishin calculus, the logic of (not necessarily distributive) de Morgan lattices, and the multiplicative-additive fragment of linear logic.
Submission history
From: Willem Conradie [view email][v1] Mon, 28 Mar 2016 09:22:03 GMT (74kb)
[v2] Mon, 4 Apr 2016 08:43:35 GMT (74kb)
Link back to: arXiv, form interface, contact.