Uniform Interpolation

TL;DR

This paper explores uniform interpolation in propositional logics, highlighting Pitts' theorem for intuitionistic logic, its semantic proof via bisimulation quantifiers, and its connections to categorical logic, algebra, and model theory.

Contribution

It presents a semantic proof of uniform interpolation for intuitionistic logic and discusses its generalizations and connections to other areas of logic.

Findings

Uniform interpolation holds for intuitionistic propositional logic.

Semantic proof via definability of bisimulation quantifiers.

Connections to categorical logic, algebra, and model theory.

Abstract

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.