Event Detail

The intuitionistic logic CD of constant domains is axiomatized by adding the schema (∀ x)(C ∨ A(x)) → C ∨ (∀ x)A(x) (x is not free in C) to the familiar axiomatization of intuitionistic predicate logic. CD is sound and complete for Kripke semantics with constant individual domains. The 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 the interpolation theorem fails for CD: the provable implication ((∀ x)(∃ y)(Py&(Qy → Rx))&¬ (∀ x)Rx) → ((∀ x)(Px → (Qx ∨ r)) → r) does not have an interpolant. Posted as http://arxiv.org/abs/1202.3519. This is a joint work with Grigory Olkhovikov (Ural State University) and Alasdair Urquhart (University of Toronto).