Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents

Tim Lyon*, Alwen Tiu, Rajeev Goré, Ranald Clouston

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    12 Citations (Scopus)

    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.

    Original languageEnglish
    Title of host publication28th EACSL Annual Conference on Computer Science Logic, CSL 2020
    EditorsMaribel Fernandez, Anca Muscholl
    PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
    ISBN (Electronic)9783959771320
    DOIs
    Publication statusPublished - Jan 2020
    Event28th EACSL Annual Conference on Computer Science Logic, CSL 2020 - Barcelona, Spain
    Duration: 13 Jan 202016 Jan 2020

    Publication series

    NameLeibniz International Proceedings in Informatics, LIPIcs
    Volume152
    ISSN (Print)1868-8969

    Conference

    Conference28th EACSL Annual Conference on Computer Science Logic, CSL 2020
    Country/TerritorySpain
    CityBarcelona
    Period13/01/2016/01/20

    Fingerprint

    Dive into the research topics of 'Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents'. Together they form a unique fingerprint.

    Cite this