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)
  Copy   BIBTEX

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.

Links

PhilArchive

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
Maehara-style modal nested calculi.Roman Kuznets & Lutz Straßburger - 2019 - Archive for Mathematical Logic 58 (3-4):359-385.
Gentzen sequent calculi for some intuitionistic modal logics.Zhe Lin & Minghui Ma - 2019 - Logic Journal of the IGPL 27 (4):596-623.
On the unity of logic.Jean-Yves Girard - 1993 - Annals of Pure and Applied Logic 59 (3):201-217.
A note on the interpolation property in tense logic.Frank Wolter - 1997 - Journal of Philosophical Logic 26 (5):545-551.
Prefixed tableaus and nested sequents.Melvin Fitting - 2012 - Annals of Pure and Applied Logic 163 (3):291 - 313.
Uniform interpolation and sequent calculi in modal logic.Rosalie Iemhoff - 2019 - Archive for Mathematical Logic 58 (1-2):155-181.

Analytics

Added to PP
2020-02-03

Downloads
175 (#103,039)

6 months
46 (#77,912)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Tim Lyon
Technische Universität Dresden

References found in this work

No references found.

Add more references