Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi
Logic in Computer Science
2023-08-01 v1 Logic
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.
Keywords
Cite
@article{arxiv.1601.05656,
title = {Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi},
author = {Roman Kuznets},
journal= {arXiv preprint arXiv:1601.05656},
year = {2023}
}