Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi

TL;DR

This paper extends a general proof method for Craig and Lyndon Interpolation to labelled sequent calculi, providing criteria based on Kripke frames that guarantee the interpolation property for various modal logics.

Contribution

It adapts a previous method to labelled sequents and identifies frame conditions that ensure interpolation, covering modal cube and transitive Geach logics.

Findings

Frame classes definable by Horn formulas have the IP.

The method applies to modal cube and infinite transitive Geach logics.

Provides criteria for guaranteeing IPs in labelled sequent calculi.

Abstract

We have recently presented a general method of proving the fundamental logical properties of Craig and Lyndon Interpolation (IPs) by induction on derivations in a wide class of internal sequent calculi, including sequents, hypersequents, and nested sequents. Here we adapt the method to a more general external formalism of labelled sequents and provide sufficient criteria on the Kripke-frame characterization of a logic that guarantee the IPs. In particular, we show that classes of frames definable by quantifier-free Horn formulas correspond to logics with the IPs. These criteria capture the modal cube and the infinite family of transitive Geach logics.