Algorithmic correspondence and canonicity for non-distributive logics

DOI10.1016/J.APAL.2019.04.003MaRDI QIDQ2273010zbMATHOpenAlexWikidataFDO

Authors Willem Conradie, Alessandra Palmigiano

Publication date 18 September 2019

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1603.08515

zbMATH Keywords

modal logicsubstructural logicscanonicityalgorithmic correspondenceSahlqvist correspondencenon-distributive lattices

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Modal logic (including the logic of norms) (03B45) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Logical aspects of lattices and related structures (03G10) Lattices and duality (06D50) Stone spaces (Boolean spaces) and related structures (06E15)

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.

Recommendations

• Algorithmic correspondence and canonicity for distributive modal logic
• Algorithmic correspondence and canonicity for possibility semantics
• scientific article; zbMATH DE number 1989651
• Canonical extensions and Kripke-Galois semantics for non-distributive logics
• Algebraization of Non-structural Logics
• Canonicity results for mu-calculi: an algorithmic approach
• Algorithmic correspondence for intuitionistic modal mu-calculus
• scientific article; zbMATH DE number 67027
• Canonicity results of substructural and lattice-based logics
• Nonmonotonic Logics and Their Algebraic Foundations

Cites work

• scientific article; zbMATH DE number 3494368 (Why is no real title available?)
• scientific article; zbMATH DE number 3499717 (Why is no real title available?)
• scientific article; zbMATH DE number 1226180 (Why is no real title available?)
• scientific article; zbMATH DE number 549966 (Why is no real title available?)
• scientific article; zbMATH DE number 1748069 (Why is no real title available?)
• scientific article; zbMATH DE number 945663 (Why is no real title available?)
• scientific article; zbMATH DE number 898142 (Why is no real title available?)
• scientific article; zbMATH DE number 908162 (Why is no real title available?)
• scientific article; zbMATH DE number 7243670 (Why is no real title available?)
• scientific article; zbMATH DE number 5046779 (Why is no real title available?)
• A Multi-type Calculus for Inquisitive Logic
• A Sahlqvist theorem for distributive modal logic
• A Sahlqvist theorem for substructural logic
• A bimodal perspective on possibility semantics
• A formalization of the propositional calculus of H-B logic
• A fresh perspective on canonical extensions for bounded lattices.
• A new proof of Sahlqvist's theorem on modal definability and completeness
• Algebraic modal correspondence: Sahlqvist and beyond
• Algebraic semantics and model completeness for intuitionistic public announcement logic
• Algorithmic correspondence and canonicity for distributive modal logic
• Algorithmic correspondence and canonicity for possibility semantics
• Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
• Algorithmic correspondence for intuitionistic modal mu-calculus
• Boolean Algebras with Operators. Part I
• Bounded lattice expansions
• Canonical extensions and relational completeness of some substructural logics
• Canonicity results for mu-calculi: an algorithmic approach
• Categories: how I learned to stop worrying and love two sorts
• Constructive canonicity for lattice-based fixed point logics
• Constructive canonicity in non-classical logics
• Context Algebras, Context Frames, and Their Discrete Duality
• Dual characterizations for finite lattices via correspondence theory for monotone modal logic
• Dualities for structures of applied logics
• Duality via Truth: Semantic frameworks for lattice-based logics
• Elementary canonical formulae: extending Sahlqvist's theorem
• Functional translation and second-order frame properties of modal logics
• Generalized Galois logics. Relational semantics of nonclassical logical calculi
• Generalized Kripke frames
• Generalized Kripke semantics for the Lambek-Grishin calculus
• Hybrid logics with Sahlqvist axioms
• Jónsson-style canonicity for ALBA-inequalities
• Lattice logic properly displayed
• Minimal predicates, fixed-points, and definability
• Modal and temporal extensions of non-distributive propositional logics
• Modal frame correspondences and fixed-points
• Multi-type display calculus for dynamic epistemic logic
• Multi-type display calculus for propositional dynamic logic
• Multi-type display calculus for semi De Morgan logic
• On Sahlqvist theory for hybrid logics
• On logics with coimplication
• On modal logic with an intuitionistic base
• On the canonicity of Sahlqvist identities
• Order-dual relational semantics for non-distributive propositional logics
• Order-dual relational semantics for non-distributive propositional logics: a general framework
• Positive modal logic
• Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic
• Referential semantics: duality and applications
• Relational semantics for full linear logic
• Residuated lattices. An algebraic glimpse at substructural logics
• Sahlqvist correspondence for modal mu-calculus
• Sahlqvist theory for impossible worlds
• Sahlqvist via translation
• Sahlqvist's theorem for Boolean algebras with operators with an application to cylindric algebras
• Semantic analysis of orthologic
• Semi-de Morgan algebras
• Stone duality for lattice expansions
• Stone duality for lattices
• Symmetric categorial grammar
• THE LOGIC OF RESOURCES AND CAPABILITIES
• The truth about algorithmic problems in correspondence theory
• TiRS graphs and TiRS frames: a new setting for duals of canonical extensions
• Topological duality and lattice expansions. I: A topological construction of canonical extensions.
• Toward an epistemic-logical theory of categorization
• Unified correspondence
• Unified correspondence and proof theory for strict implication
• Unified correspondence as a proof-theoretic tool

Cited in

(44)

• Sahlqvist theory for impossible worlds
• Syntactic Completeness of Proper Display Calculi
• Labelled calculi for the logics of rough concepts
• Algebraic proof theory for LE-logics
• Modal reduction principles: a parametric shift to graphs
• A non-distributive logic for semiconcepts and its modal extension with semantics based on Kripke contexts
• Algorithmic Correspondence for Relevance Logics I. The Algorithm $$\mathsf {PEARL}$$
• Modelling socio-political competition
• Algorithmic correspondence and canonicity for distributive modal logic
• Toward an epistemic-logical theory of categorization
• Rough concepts
• Definable operators on stable set lattices
• Canonicity results of substructural and lattice-based logics
• Slanted canonicity of analytic inductive inequalities
• Modal inverse correspondence via ALBA
• Constructive canonicity for lattice-based fixed point logics
• Sahlqvist via translation
• Subordination algebras as semantic environment of input/output logic
• Canonicity results for mu-calculi: an algorithmic approach
• Dual characterizations for finite lattices via correspondence theory for monotone modal logic
• Algebraic modal correspondence: Sahlqvist and beyond
• Unified correspondence and proof theory for strict implication
• Semi De Morgan logic properly displayed
• A Sahlqvist theorem for distributive modal logic
• Positive modal logic beyond distributivity
• Algorithmic correspondence and canonicity for possibility semantics
• Non-distributive description logic
• Correspondence theory for generalized modal algebras
• Reasoning with incomplete information in generalized Galois logics without distribution: the case of negation and modal operators
• scientific article; zbMATH DE number 5173450 (Why is no real title available?)
• Semantic Analysis of Subexponential Modalities in Distributive Non-commutative Linear Logic
• Residuation algebras with functional duals
• Polynomial-time checking of generalized Sahlqvist syntactic shape
• scientific article; zbMATH DE number 7243670 (Why is no real title available?)
• Labelled calculi for lattice-based modal logics
• Editorial: Canonicity and correspondence for nonclassical logics
• Modal translation of substructural logics
• Non-normal modal logics and conditional logics: semantic analysis and proof theory
• Unified correspondence
• Algorithmic correspondence for intuitionistic modal mu-calculus
• scientific article; zbMATH DE number 1989651 (Why is no real title available?)
• Unified correspondence as a proof-theoretic tool
• Linear Logic Properly Displayed
• Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras via an implementation of the algorithm \textsf{PEARL}

Describes a project that uses

Uses Software

• SQEMA

This page was built for publication: Algorithmic correspondence and canonicity for non-distributive logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2273010)