Interpolation for intermediate logics via injective nested sequents

摘要

We introduce a novel, semantically inspired method of constructing nested sequent calculi for propositional intermediate logics. Applying recently developed methods for proving Craig interpolation to these nested sequent calculi, we obtain constructive proofs of the interpolation property for most non-trivial interpolable intermediate logics, as well as Lyndon interpolation for Godel logic. Finally, we provide a prototype implementation combining proof search and countermodel construction.