Dual characterizations for finite lattices via correspondence theory for monotone modal logic

Abstract

We establish a formal connection between algorithmic correspondence theory and certain dual characterization results for finite lattices, similar to Nation's characterization of a hierarchy of pseudovarieties of finite lattices, progressively generalizing finite distributive lattices. This formal connection is mediated through monotone modal logic. Indeed, we adapt the correspondence algorithm ALBA to the setting of monotone modal logic, and we use a certain duality-induced encoding of finite lattices as monotone neighbourhood frames to translate lattice terms into formulas in monotone modal logic.

References in corpus (5)

• Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
• Constructive Canonicity of Inductive Inequalities
• Canonicity and Relativized Canonicity via Pseudo-Correspondence: an Application of ALBA
• Unified Correspondence and Proof Theory for Strict Implication
• Constructive canonicity for lattice-based fixed point logics

Cited by in corpus (7)

• Sahlqvist theory for impossible worlds
• Sahlqvist via Translation
• Constructive Canonicity of Inductive Inequalities
• Unified Correspondence and Proof Theory for Strict Implication
• Canonicity and Relativized Canonicity via Pseudo-Correspondence: an Application of ALBA
• Non normal logics: semantic analysis and proof theory
• Non-normal logics: semantic analysis and proof theory (extended version)