Uniform Lyndon interpolation property in propositional modal logics

TL;DR

This paper introduces the uniform Lyndon interpolation property (ULIP) in propositional modal logics, demonstrating its presence in several key systems and providing complexity bounds for certain cases.

Contribution

It defines ULIP as a new strengthening of existing interpolation properties and proves its validity in multiple modal logics, extending the understanding of interpolation in modal logic.

Findings

ULIP holds for ${f K}$, ${f KB}$, ${f GL}$, and ${f Grz}$.

Modified Visser's proofs using layered bisimulations.

New upper bounds on complexity of uniform interpolants for ${f GL}$ and ${f Grz}$.

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 ${\bf K}$, ${\bf KB}$, ${\bf GL}$ and ${\bf 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 ${\bf GL}$ and ${\bf Grz}$.