Algorithmic correspondence and canonicity for non-distributive logics
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.
Keywords
Cite
@article{arxiv.1603.08515,
title = {Algorithmic correspondence and canonicity for non-distributive logics},
author = {Willem Conradie and Alessandra Palmigiano},
journal= {arXiv preprint arXiv:1603.08515},
year = {2016}
}
Comments
This article is part of a research program called "Unified Correspondence". There is bound to be textual overlap with our paper on Constructive Canonicity of Inductive Inequalities (arXiv:1603.08341). The same proof strategy works in both cases, but there are many subtle yet crucial differences