# [FOM] Failure of interpolation in CD

Alasdair Urquhart urquhart at cs.toronto.edu
Thu Apr 5 15:15:52 EDT 2012

```
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
(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.

```