A simple algebraic proof of the equational interpolation theorem (Q1173754)

In this paper, the author gives a proof of the following interpolation theorem for equational logic: Let \(X\) and \(Y\) be sets of equations such that \(X\models Y\). Then there exists a set \(I\) of interpolant equations, with all its non-logical symbols both in \(X\) and \(Y\), such that \(X\models I\) and \(I\models Y\). The result is obtained through a simple algebraic construction. Many- sorted algebras are involved and the necessary extension of the notion of a signature is made, but the result can also be taken within traditional equational logic.