Interpolation theorems for intuitionistic predicate logic (Q5957915)

For the classical first-order logic the Craig interpolation theorem may be extended to partitions \(\Gamma;\Gamma^\prime\vdash\Delta;\Delta^\prime\) of the sequent \(\Gamma,\Gamma^\prime\vdash\Delta,\Delta^\prime\) meaning that, for each partition, there is an interpolant \(I\) such that both sequents \(\Gamma\vdash\Delta,I\) and \(I,\Gamma^\prime\vdash\Delta^\prime\) are provable. The same extension of the Craig interpolation theorem to the case of intuitionistic predicate logic is not possible. However, in this paper the author presents a version of such an extension true for intuitionistic propositional calculus and a more complicated version for the predicate language case.