First-order interpolation derived from propositional interpolation (Q2193292)

While interpolation properties in a propositional logic $L$ usually hinge upon the underlying algebras of $L$, the study of interpolation in first-order logics does not have a similar algebraic flavor. In the paper under review the authors give a method to reduce first-order to propositional interpolation. Suitable skolemizations and Herbrand expansions are constructed which, combined with a \textit{propositional} interpolant, yield a \textit{first-order} interpolant. The proof-theoretic constructions of this paper are applicable to lattice-based finite-valued logics and to the weak quantifier and subprenex fragments of infinitely-valued first-order Gödel logic. Interpolation turns out to be decidable for these logics.