ANALYTIC CUT AND INTERPOLATION FOR BI-INTUITIONISTIC LOGIC
Tomasz Kowalski, Hiroakira Ono · The Review of Symbolic Logic · 2016
Abstract 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.