Uniform Lyndon interpolation property in propositional modal logics

Abstract

We introduce and investigate the notion of uniform Lyndon interpolation property (ULIP) which is a strengthening of both uniform interpolation property and Lyndon interpolation property. We prove several propositional modal logics including $\mathbf{K}$, $\mathbf{KB}$, $\mathbf{GL}$ and $\mathbf{Grz}$ enjoy ULIP. Our proofs are modifications of Visser's proofs of uniform interpolation property using layered bisimulations. Also we give a new upper bound on the complexity of uniform interpolants for $\mathbf{GL}$ and $\mathbf{Grz}$.

arXiv comment21 pages