Extensions of $$\textsf{K5}$$: Proof Theory and Uniform Lyndon Interpolation
Iris van der Giessen, Raheleh Jalali, Roman Kuznets · Lecture notes in computer science · 2023
Abstract We introduce a Gentzen-style framework, calledlayered sequent calculi, for modal logic $$\textsf{K5}$$ and its extensions $$\textsf{KD5}$$ , $$\textsf{K45}$$ , $$\textsf{KD45}$$ , $$\textsf{KB5}$$ , and $$\textsf{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 $$\textsf{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.