English

Interpolation in Proof Theory

Logic in Computer Science 2026-02-19 v1

Abstract

This chapter provides a comprehensive overview of proof-theoretic methods for establishing interpolation properties across a range of logics, including classical, intuitionistic, modal, and substructural logics. Central to the discussion are two foundational techniques: Maehara's method for Craig interpolation and Pitts' method for uniform interpolation. The chapter demonstrates how these methods lead to results on the existence of well-behaved proof systems in the contemporary framework of universal proof theory and how they provide a road map for constructing interpolation proofs using modern proof formalisms. The emphasis of the chapter is on constructive, modular, and syntax-driven techniques that illuminate deeper connections between interpolation properties and proof systems.

Keywords

Cite

@article{arxiv.2602.16318,
  title  = {Interpolation in Proof Theory},
  author = {Iris van der Giessen and Raheleh Jalali and Roman Kuznets},
  journal= {arXiv preprint arXiv:2602.16318},
  year   = {2026}
}

Comments

The article will appear in Balder ten Cate, Jean Christoph Jung, Patrick Koopmann, Christoph Wernhard and Frank Wolter, editors. Theory and Applications of Craig Interpolation. Ubiquity Press, 2026

R2 v1 2026-07-01T10:41:03.683Z