We propose a new proof theoretical method for proving Lyndon interpolation. Our proof does not use the sequent calculus but is based on a generalization of the splitting lemma in deep inference. We then formulate the interpolation theorem as a decomposition of a derivation into an up-fragment and a down-fragment. This can be seen as (i) a strengthening of the standard formulation of the interpolation theorem, and (ii) a generalization of the cut elimination theorem. We demonstrate the flexibility of our approach by applying it to linear logic, classical logic, and modal logics. For this, we also introduce novel cut-free proof systems for several modal logics in deep inference.

翻译：暂无翻译