[FOM] Failure of interpolation in CD

[Alasdair Urquhart]

   Failure of interpolation for intuitionistic logic of constant domains

Posted as http://arxiv.org/abs/1202.3519.

Grigori Mints (Stanford University), Grigory Olkhovikov (Ural State 
University), Alasdair  Urquhart (University of Toronto)

           Intuitionistic logic CD of constant domains is axiomatized by
adding the schema
        (Ax)(C v A(x)) => C v (Ax)A(x) (x is not free in C) to familiar 
axiomatization of intuitionistic predicate logic. CD is sound
and complete for Kripke semantics with constant individual domains.
     Interpolation theorem says that for any provable implication A=>B 
there is an interpolant I such that A=>I and I=>B are both provable, and I
contains only predicates common to A and B.

     There are at least two claimed proofs of the interpolation theorem for
CD, both published in The Journal of Symbolic Logic (v. 42, 1977 and v.46,
1981). We prove that in fact interpolation theorem fails for CD: provable
implication
((Ax)(Ey)(Py & (Qy=>Rx)) & ~(Ax)Rx) => ((Ax)(Px=>(Qx v r))=>r)
does not have an interpolant.