  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 (G. Mints, G. K. Olkhovikov and A. Urquhart. Failure of
Interpolation in Constant Domain Intuitionistic Logic. Journal of Symbolic
Logic, 78: 937--950 (2013)). More precisely, we show that there is a valid
implication $\phi \rightarrow \psi$ with no interpolant (i.e. a formula
$\theta$ in the intersection of the vocabularies of $\phi$ and $\psi$ such that
both $\phi \rightarrow \theta$ and $\theta \rightarrow \psi$ are valid).
Importantly, this result does not contradict the unfortunately named `Craig
interpolation' theorem established by Rauszer in (Cecylia Rauszer. Craig
Interpolation Theorem for an Extention of Intuitionistic Logic. Bull. Ac. Pol.
Sc., 25(4), 337--341 (1977)) since that article is about the property more
correctly named `deductive interpolation' (see Galatos, Jipsen, Kowalski and
Ono's use of this term in N. Galatos, P. Jipsen, T. Kowalski, \& H. Ono.
Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Studies in
Logic and the Foundations of Mathematics, Vol. 151. Amsterdam: Elsevier B. V.
(2007)) 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.
