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

In Maribel Fernandez & Anca Muscholl (eds.), 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Dagstuhl, Germany: pp. 1-16 (2020)
Download Edit this record How to cite View on PhilPapers
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.
Categories
(categorize this paper)
PhilPapers/Archive ID
LYOSIF
Upload history
First archival date: 2020-02-03
Latest version: 2 (2020-02-03)
View other versions
Added to PP index
2020-02-03

Total views
25 ( #50,381 of 52,731 )

Recent downloads (6 months)
13 ( #38,229 of 52,731 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.