2026-07-21T14:19:12Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11671 2024-03-06T10:48:45Z ddc:004 open_access

Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents Lyon, Tim Tiu, Alwen Goré, Rajeev Clouston, Ranald Bi-intuitionistic logic Interpolation Nested calculi Proof theory Sequents Tense logics 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Tim Lyon and Alwen Tiu and Rajeev Goré and Ranald Clouston 2020 Is Part Of LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2020.28 urn:nbn:de:0030-drops-116713 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.28 eng https://creativecommons.org/licenses/by/3.0/legalcode