Extensions of K5: Proof Theory and Uniform Lyndon Interpolation

TL;DR

This paper develops a layered sequent calculus framework for modal logic K5 and its extensions, providing decision procedures and a constructive proof of the uniform Lyndon interpolation property, advancing proof theory and interpolation understanding.

Contribution

It introduces layered sequent calculi for K5 extensions, offers optimal decision procedures, and provides the first syntactic proof of ULIP for K5 using model-theoretic methods.

Findings

Decision procedures are optimal for all considered logics.

Constructive proof of ULIP for K5 established.

Model-theoretic methods validate interpolant correctness.

Abstract

We introduce a Gentzen-style framework, called layered sequent calculi, for modal logic K5 and its extensions KD5, K45, KD45, KB5, and S5 with the goal to investigate the uniform Lyndon interpolation property (ULIP), which implies both the uniform interpolation property and the Lyndon interpolation property. We obtain complexity-optimal decision procedures for all logics and present a constructive proof of the ULIP for K5, which to the best of our knowledge, is the first such syntactic proof. To prove that the interpolant is correct, we use model-theoretic methods, especially bisimulation modulo literals.