Analytic cut and interpolation for bi-intuitionistic logic

Review of Symbolic Logic 10 (2):259-283 (2017)
  Copy   BIBTEX


We prove that certain natural sequent systems for bi-intuitionistic logic have the analytic cut property. In the process we show that the (global) subformula property implies the (local) analytic cut property, thereby demonstrating their equivalence. Applying a version of Maehara technique modified in several ways, we prove that bi-intuitionistic logic enjoys the classical Craig interpolation property and Maximova variable separation property; its Halldén completeness follows.



    Upload a copy of this work     Papers currently archived: 91,386

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

Interpolation theorems for intuitionistic predicate logic.G. Mints - 2001 - Annals of Pure and Applied Logic 113 (1-3):225-242.
Interpolation in fragments of classical linear logic.Dirk Roorda - 1994 - Journal of Symbolic Logic 59 (2):419-444.
On the interpolation property of some intuitionistic modal logics.C. Luppi - 1996 - Archive for Mathematical Logic 35 (3):173-189.
Hypersequent calculi for intuitionistic logic with classical atoms.Hidenori Kurokawa - 2010 - Annals of Pure and Applied Logic 161 (3):427-446.
Interpolation property for bicartesian closed categories.Djordje Čubrić - 1994 - Archive for Mathematical Logic 33 (4):291-319.


Added to PP

51 (#305,341)

6 months
7 (#411,886)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Hiroakira Ono
Japan Advanced Institute of Science and Technology
Tomasz Kowalski
La Trobe University

References found in this work

On logics with coimplication.Frank Wolter - 1998 - Journal of Philosophical Logic 27 (4):353-387.
Varieties Of Tense Algebras.Tomasz Kowalski - 1998 - Reports on Mathematical Logic:53-95.

View all 9 references / Add more references