Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents

TL;DR

This paper introduces a syntactic method using nested sequent calculi to prove Craig interpolation for various modal and intuitionistic logics, including tense and bi-intuitionistic logics, without semantic arguments.

Contribution

It presents a direct, purely syntactic proof of Craig interpolation for complex logics with nested sequent calculi, introducing an orthogonality condition for duality of interpolants.

Findings

Proves Craig interpolation for classical tense logic and its extensions.

Establishes interpolation for bi-intuitionistic logic.

Uses nested sequent calculi without semantic embeddings.

Abstract

We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants.