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

TL;DR

This paper develops a formal link between algorithmic correspondence theory and dual lattice characterizations using monotone modal logic, generalizing finite distributive lattices.

Contribution

It adapts the ALBA correspondence algorithm to monotone modal logic and encodes finite lattices as monotone neighborhood frames for analysis.

Findings

Established a formal connection between correspondence theory and lattice dualities.

Adapted ALBA algorithm for monotone modal logic.

Provided a duality-based encoding of finite lattices.

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.