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)

Authors
Tim Lyon
Vienna University of Technology
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.
Keywords Bi-intuitionistic logic  Interpolation  Nested calculi  Proof theory  Sequents  Tense logics
Categories (categorize this paper)
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles

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 index
2020-02-03

Total views
10 ( #775,385 of 2,286,122 )

Recent downloads (6 months)
10 ( #91,135 of 2,286,122 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature