arXiv:2611.16481 · v1

Strong Lyndon Interpolation for Multi-Modal Logics with Converses: A Constructive Approach with Tree Sequents

首次提交 2026-11-12 16:51

版本更新 2026-11-12 16:51

雷达观测 2026-11-13 14:15

摘要

Grammar logics with converses are multi-modal logics that generalize tense logics and whose frame conditions are determined by context-free production rules. We study the strong Lyndon interpolation property (strong LIP) for these logics, which requires interpolants to respect both the polarities of propositional atoms and the indices of modalities. We show that the strong LIP properly strengthens the Lyndon interpolation property over grammar logics, since it fails for certain grammar logics with bridge axioms, i.e., path axioms relating modalities with distinct indices. We then prove that every bridge-free grammar logic, possibly extended with seriality axioms, has the strong LIP. This class includes the multi-modal tense logics obtained by imposing any combination of seriality, reflexivity, transitivity, symmetry, and Euclideanity on each pair of converse modalities. Our proof is constructive and purely syntactic, and is based on tree sequent calculi. Because standard methods for computing interpolants with tree and nested sequents may introduce modalities whose indices are not common to both sides of an implication, we introduce a novel tripartite partition method. It sorts the labels of a proof into common labels and labels private to the left or right component, and only lets relational atoms pointing to common labels contribute modalities to interpolants. Given a proof of an implication, our method computes a strong Lyndon interpolant together with proofs of its correctness.

作者备注：in review