Distribution-Free Modal Logics: Sahlqvist -- Van Benthem Correspondence
Chrysafis, Hartonas
TL;DR
This paper extends the classical Sahlqvist--Van Benthem correspondence to distribution-free modal logic (DfML) by embedding DfML into a sorted modal companion and employing duality with sorted residuated frames. It develops a reductionist pipeline that translates sequents into canonical Sahlqvist form, computes t-invariance constraints, generates guarded second-order translations, and eliminates second-order quantifiers to obtain first-order local correspondents. The core contributions are the formalization of sorted frame semantics, the detailed algorithmic steps (Step 1–6) for the correspondence, and the handling of box/diamond interactions, negation, and implication within the distribution-free setting. The framework is scalable and generalizes to substructural logics, with connections to Ackermann-style quantifier elimination and a unified algebraic perspective on correspondence theory. Together, these results provide a concrete, transferable method for deriving first-order correspondents across non-classical logics while preserving classical results as a special case.
Abstract
We present an extension and generalization of Sahlqvist--Van Benthem correspondence to the case of distribution-free modal logic, with, or without negation and/or implication connectives. We follow a reductionist strategy, reducing the correspondence problem at hand to the same problem, but for a suitable system of sorted modal logic (the modal companion of the distribution-free system). The reduction, via a fully abstract translation, builds on duality between normal lattice expansions and sorted residuated frames with relations (a generalization of classical Kripke frames with relations). The approach is scalable and it can be generalized to other systems, with or without distribution, such as distributive modal logic, or substructural logics with, or without additional modal operators.