Algorithmic correspondence and canonicity for non-distributive logics

DOI10.1016/J.APAL.2019.04.003zbMATH Open1477.03046arXiv1603.08515OpenAlexW2964164692WikidataQ128059089 ScholiaQ128059089MaRDI QIDQ2273010FDOQ2273010

Authors: Willem Conradie, Alessandra Palmigiano 

Publication date: 18 September 2019

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

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.

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

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
• Canonicity results of substructural and lattice-based logics
• Nonmonotonic Logics and Their Algebraic Foundations

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)

Cites Work

• Stone duality for lattices
• Generalized Galois logics. Relational semantics of nonclassical logical calculi
• Title not available (Why is that?)
• Title not available (Why is that?)
• Boolean Algebras with Operators. Part I
• Positive modal logic
• Title not available (Why is that?)
• Residuated lattices. An algebraic glimpse at substructural logics
• Relational semantics for full linear logic
• Title not available (Why is that?)
• Canonical extensions and relational completeness of some substructural logics
• Bounded lattice expansions
• Generalized Kripke frames
• A formalization of the propositional calculus of H-B logic
• Constructive canonicity in non-classical logics
• Semantic analysis of orthologic
• Semi-de Morgan algebras
• A SAHLQVIST THEOREM FOR SUBSTRUCTURAL LOGIC
• Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
• On logics with coimplication
• Referential semantics: duality and applications
• Symmetric categorial grammar
• Algebraic semantics and model completeness for intuitionistic public announcement logic
• Algorithmic correspondence and canonicity for distributive modal logic
• A fresh perspective on canonical extensions for bounded lattices.
• Title not available (Why is that?)
• On the canonicity of Sahlqvist identities
• Algebraic modal correspondence: Sahlqvist and beyond
• Modal frame correspondences and fixed-points
• Elementary canonical formulae: extending Sahlqvist's theorem
• The truth about algorithmic problems in correspondence theory
• Title not available (Why is that?)
• Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic
• Hybrid logics with Sahlqvist axioms
• A Sahlqvist theorem for distributive modal logic
• Sahlqvist correspondence for modal mu-calculus
• A new proof of Sahlqvist's theorem on modal definability and completeness
• Minimal predicates, fixed-points, and definability
• Title not available (Why is that?)
• Algorithmic correspondence for intuitionistic modal mu-calculus
• Unified Correspondence
• 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.
• On modal logic with an intuitionistic base
• Duality via Truth: Semantic frameworks for lattice-based logics
• Sahlqvist's theorem for Boolean algebras with operators with an application to cylindric algebras
• Title not available (Why is that?)
• Context Algebras, Context Frames, and Their Discrete Duality
• Title not available (Why is that?)
• Functional translation and second-order frame properties of modal logics
• A Multi-type Calculus for Inquisitive Logic
• Sahlqvist theory for impossible worlds
• Constructive canonicity for lattice-based fixed point logics
• Title not available (Why is that?)
• Unified correspondence as a proof-theoretic tool
• Order-dual relational semantics for non-distributive propositional logics: a general framework
• Order-dual relational semantics for non-distributive propositional logics
• Modal and temporal extensions of non-distributive propositional logics
• Generalized Kripke semantics for the Lambek-Grishin calculus
• Lattice logic properly displayed
• Multi-type display calculus for semi De Morgan logic
• A bimodal perspective on possibility semantics
• Categories: How I Learned to Stop Worrying and Love Two Sorts
• Multi-type display calculus for dynamic epistemic logic
• Multi-type display calculus for propositional dynamic logic
• Jónsson-style canonicity for ALBA-inequalities
• THE LOGIC OF RESOURCES AND CAPABILITIES
• Title not available (Why is that?)
• Dual characterizations for finite lattices via correspondence theory for monotone modal logic
• Canonicity results for mu-calculi: an algorithmic approach
• On Sahlqvist theory for hybrid logics
• Unified correspondence and proof theory for strict implication
• Title not available (Why is that?)
• Title not available (Why is that?)
• Stone duality for lattice expansions
• Algorithmic correspondence and canonicity for possibility semantics

Cited In (31)

• Title not available (Why is that?)
• Non-normal modal logics and conditional logics: semantic analysis and proof theory
• Labelled calculi for the logics of rough concepts
• Labelled calculi for lattice-based modal logics
• Title not available (Why is that?)
• Syntactic Completeness of Proper Display Calculi
• Title not available (Why is that?)
• A Sahlqvist theorem for distributive modal logic
• Title not available (Why is that?)
• A non-distributive logic for semiconcepts and its modal extension with semantics based on Kripke contexts
• Algorithmic correspondence and canonicity for possibility semantics
• Reasoning with Incomplete Information in Generalized Galois Logics Without Distribution: The Case of Negation and Modal Operators
• Algorithmic Correspondence for Relevance Logics I. The Algorithm $$\mathsf {PEARL}$$
• Subordination algebras as semantic environment of input/output logic
• Residuation algebras with functional duals
• Semi De Morgan logic properly displayed
• Definable operators on stable set lattices
• Positive modal logic beyond distributivity
• Modelling socio-political competition
• Correspondence theory for generalized modal algebras
• Semantic Analysis of Subexponential Modalities in Distributive Non-commutative Linear Logic
• Modal translation of substructural logics
• Polynomial-time checking of generalized Sahlqvist syntactic shape
• Linear Logic Properly Displayed
• Rough concepts
• Canonicity results for mu-calculi: an algorithmic approach
• Algebraic proof theory for LE-logics
• Modal reduction principles: a parametric shift to graphs
• Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras via an implementation of the algorithm \textsf{PEARL}
• Constructive canonicity for lattice-based fixed point logics
• Non-distributive description logic

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)