CRAIG INTERPOLATION THEOREM FAILS IN BI-INTUITIONISTIC PREDICATE LOGIC

In this article we show that bi-intuitionistic predicate logic lacks the Craig Interpolation Property. We proceed by adapting the counterexample given by Mints, Olkhovikov and Urquhart for intuitionistic predicate logic with constant domains [13]. More precisely, we show that there is a valid implication phi ->psi with no interpolant. Importantly, this result does not contradict the unfortunately named `Craig interpolation' theorem established by Rauszer in [24] since that article is about the property more correctly named `deductive interpolation' (see Galatos, Jipsen, Kowalski and Ono's use of this term in [5]) for global consequence. Given that the deduction theorem fails for bi-intuitionistic logic with global consequence, the two formulations of the property are not equivalent.