Interpolation theorems for intuitionistic predicate logic Original Research Article

Craig interpolation theorem (which holds for intuitionistic logic) implies that the derivability of X,X′⇒Y′ implies existence of an interpolant I in the common language of X and X′⇒Y′ such that both X⇒I and I,X′⇒Y′ are derivable. For classical logic this extends to X,X′⇒Y,Y′, but for intuitionistic logic there are counterexamples. We present a version true for intuitionistic propositional (but not for predicate) logic, and more complicated version for the predicate case.