Failure of interpolation in constant domain intuitionistic logic (Q2869908)

The intuitionistic logic of constant domains CD is obtained from intuitionistic predicate logic by adding the scheme \(\forall x\,(A\lor B)\to(A\lor\forall x\,B)\). Its modal counterpart under the Gödel-Tarski translation is the system S4+BF obtained by adding the Barcan formula to S4. NEWLINENEWLINENEWLINEThere are two published proofs that CD has the interpolation property. A model-theoretic proof was given by \textit{D. M. Gabbay} [J. Symb. Log. 42, 269--271 (1977; Zbl 0372.02016)], but that proof contained gaps. A proof-theoretic proof was proposed by \textit{E. G. K. Lopez-Escobar} [J. Symb. Log. 46, 87--88 (1981; Zbl 0469.03015)], but in a later article of the same author [J. Symb. Log. 48, 595--599 (1983; Zbl 0547.03022)] it was admitted that the earlier proof was incorrect. NEWLINENEWLINENEWLINEIn the present paper, a counterexample to the interpolation property for CD is given. Namely, the implication \(\Gamma\to\Delta\), where \(\Gamma\) is \(\forall x\exists y\,(Py\land(Qy\to Rx))\land\neg\forall x\,Rx)\) and \(\Delta\) is \(\forall x\,(Px\to(Qx\lor S))\to S\), is deducible in CD but has no interpolant in CD. Nevertheless, its modal translation has an interpolant in S4+BF.