License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2020.28
URN: urn:nbn:de:0030-drops-116713
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/11671/
Go to the corresponding LIPIcs Volume Portal

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

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

pdf-format:
LIPIcs-CSL-2020-28.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{lyon_et_al:LIPIcs:2020:11671,
  author =	{Tim Lyon and Alwen Tiu and Rajeev Gor{\'e} and Ranald Clouston},
  title =	{{Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{28:1--28:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Maribel Fern{\'a}ndez and Anca Muscholl},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/11671},
  URN =		{urn:nbn:de:0030-drops-116713},
  doi =		{10.4230/LIPIcs.CSL.2020.28},
  annote =	{Keywords: Bi-intuitionistic logic, Interpolation, Nested calculi, Proof theory, Sequents, Tense logics}
}

Keywords: Bi-intuitionistic logic, Interpolation, Nested calculi, Proof theory, Sequents, Tense logics
Collection: 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Issue Date: 2020
Date of publication: 06.01.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI