Uniform interpolation is a strengthening of interpolation that holds for certain propositional logics. The starting point of this chapter is a theorem of A. Pitts, which shows that uniform interpolation holds for intuitionistic propositional logic. We outline how this theorem may be proved semantically via the definability of bisimulation quantifiers, and how it generalizes to an open mapping theorem between Esakia spaces. We also discuss connections between uniform interpolation and research in categorical logic, algebra, and model theory.

翻译：统一插值是插值性质的强化形式，它适用于某些命题逻辑。本章的起点是A. Pitts的一个定理，该定理表明直觉主义命题逻辑满足统一插值性质。我们概述了如何通过双模拟量词的可定义性从语义角度证明该定理，以及如何将其推广为Esakia空间之间的开映射定理。我们还讨论了统一插值与范畴逻辑、代数和模型论研究之间的关联。