Algorithmic correspondence and canonicity for non-distributive logics

TL;DR

This paper extends unified correspondence theory to a broad class of non-distributive logics using algebraic semantics, introducing a syntactic class of formulas and an effective algorithm for correspondence and canonicity results.

Contribution

It introduces a general syntactic class of Sahlqvist formulas for lattice-based logics and a specialized ALBA algorithm that computes first-order correspondents and proves canonicity.

Findings

ALBA algorithm effectively computes first-order correspondents for many inequalities.

All inequalities on which ALBA succeeds are canonical.

Extends correspondence theory to substructural logics like Lambek calculus and linear logic.

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.