Modular constructive Lyndon interpolation for nondistributive logics

TL;DR

This paper proves the Lyndon interpolation property for a broad class of lattice expansion logics using a constructive, modular approach with display calculi, enabling algorithmic derivation of interpolants.

Contribution

It introduces a modular, constructive method for establishing Lyndon interpolation in basic lattice expansion logics via display calculi, applicable to axiomatic extensions.

Findings

Lyndon interpolation property established for basic lattice expansion logics.

Interpolation for extensions can be derived by verifying local properties of structural rules.

Tense version of Holliday's modal logic also enjoys Lyndon interpolation.

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.