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空间之间的开映射定理。同时，我们探讨了一致插值与范畴逻辑、代数及模型论研究之间的关联。