On the Craig-Lyndon interpolation theorem
Arnold Oberschelp · Journal of Symbolic Logic · 1968
In his paper [3] Henkin proved for a first order language with identity symbol but without operation symbols the following version of the Craig-Lyndon interpolation theorem: Theorem 1. If Γ╞Δ then there is a formula θ such that Γ ├Δand (i) any relation symbol with a positive (negative) occurrence in θ has a positive (negative) occurrence in some formula of Γ.