An interpolation theorem (Q2711348)

The author proves a Lyndon-like interpolation theorem where, for some fixed tuple \(U\) of unary predicates, all formulas under consideration have all their quantifiers explicitly relativized to one of the \(U\)'s. Under this stipulation, existential (resp., universal) quantification over \(U\) contributes a positive (resp., negative) occurrence of \(U\). It is shown that this interpolation theorem unifies a number of related results.