Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Uniform Interpolation

Sam van Gool

TL;DR

This work surveys a semantic approach to uniform interpolation for propositional logics, centering on bisimulation quantifiers and their definability. It connects semantic adjoints, Esakia duality, and categorical logic to derive uniform interpolants, and then links these semantic results to algebraic model theory via model completions. The chapter also discusses extensions to other logics, limitations, and complementary syntactic methods, highlighting both theoretical insights and practical computation considerations. Overall, the text unifies semantic, algebraic, and categorical perspectives to illuminate when and how uniform interpolation can be obtained and what it implies about the surrounding logical and model-theoretic landscape.

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.

Uniform Interpolation

TL;DR

This work surveys a semantic approach to uniform interpolation for propositional logics, centering on bisimulation quantifiers and their definability. It connects semantic adjoints, Esakia duality, and categorical logic to derive uniform interpolants, and then links these semantic results to algebraic model theory via model completions. The chapter also discusses extensions to other logics, limitations, and complementary syntactic methods, highlighting both theoretical insights and practical computation considerations. Overall, the text unifies semantic, algebraic, and categorical perspectives to illuminate when and how uniform interpolation can be obtained and what it implies about the surrounding logical and model-theoretic landscape.

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.

Paper Structure

This paper contains 12 sections, 12 theorems, 12 equations, 1 table.

Table of Contents

  1. Introduction
  2. Uniform Interpolants via Bisimulation Quantifiers
  3. Models and Bisimilarity
  4. Bisimulation Quantifiers
  5. Definability via Bounded Bisimulations
  6. Extensions of the Semantic Method to Other Logics
  7. Uniform Interpolants via Adjunction and Topology
  8. Uniform Interpolants as Adjoints
  9. Esakia Duality and Open Mappings
  10. Connections to Categorical Logic
  11. Model-complete Theories from Uniform Interpolants
  12. Syntactic Methods, Further Results and Connections

Key Result

Theorem 1

In intuitionistic logic, any propositional formula has both left and right uniform interpolants, with respect to any set of propositional variables.

Theorems & Definitions (18)

  • Theorem 1: Pitts, Pit1992
  • Definition 2
  • Definition 3
  • Lemma 4
  • Proposition 5
  • Definition 6
  • Proposition 7
  • Proposition 8
  • Lemma 9: Expansion Lemma
  • Corollary 10
  • ...and 8 more