Uniform Interpolation and Compact Congruences

The following remarkable feature of intuitionistic propositional logic (IPC) was established by A. M. Pitts in [3]. Given any formula α(x̄, ȳ) (using brackets as usual to indicate variables that may occur in the formula), there exist formulas αL(ȳ) and αR(ȳ), left and right uniform interpolants of α, respectively, such that for any formula β(ȳ, z̄), β `IPC α ⇔ β `IPC αL and α `IPC β ⇔ αR `IPC β. All seven intermediate logics admitting Craig interpolation also admit uniform interpolation; however, although the modal logic K admits both properties, its extension S4 admits only Craig interpolation and not uniform interpolation (see [1] for details and references). Uniform interpolation for a logic may be viewed as a weaker form of quantifier elimination. This idea is exploited in the monograph [1] of Ghilardi and Zawad-owski to show that under certain conditions, satisfied in particular by IPC and K, uniform interpolation for a logic implies the existence of a model completion for a corresponding variety (equational class) of algebras