Modular constructive Lyndon interpolation for nondistributive logics
Logic
2026-05-19 v1
Abstract
We establish the Lyndon interpolation property for basic lattice expansion logics (LE-logics) in arbitrary signatures using display calculi. Our approach is constructive, yielding interpolants algorithmically from derivations, and modular, in the sense that interpolation for axiomatic extensions can be obtained by verifying a local interpolation property for the analytic structural rules corresponding to the additional axioms. To this end, we identify a class of interpolation-safe structural rules preserving local Lyndon interpolation. As applications of the general framework, we show that the tense version of Holliday's fundamental modal logic enjoys the Lyndon interpolation property.
Cite
@article{arxiv.2605.17161,
title = {Modular constructive Lyndon interpolation for nondistributive logics},
author = {Andrea De Domenico and Giuseppe Greco and Alessandra Palmigiano and Apostolos Tzimoulis},
journal= {arXiv preprint arXiv:2605.17161},
year = {2026}
}