A heterogeneous interpolant

摘要: In this note we exhibit an interpolant for a certain valid implication ╞ φ → ψ, where φ and ψ come from the infinitary language Lω1ω1. The existence of this interpolant follows from Takeuti’s heterogeneous interpolation theorem [5], but unfortunately the proof in [5] is not explicit enough to allow one to find the interpolant explicitly. Takeuti’s theorem asserts the existence of an interpolant in the class Lω1ω1 of heterogeneous formulas, which admits the rules of formation of Lω1ω1 plus the following additional rule: