Interpolation in Proof Theory

TL;DR

The chapter addresses interpolation properties across classical, intuitionistic, modal, and substructural logics using proof-theoretic, constructive methods. It centers on Maehara's constructive CIP method, which extracts interpolants from sequent proofs of $\varphi \rightarrow \psi$, and Pitts' syntactic UIP method, notably for ${\sf IPC}$ and its extensions, with formalizations enabling automated interpolant computation. It further explores the shift to richer proof formalisms (labelled, hyper-, and nested sequents) and the role of semi-analytic rules in universal proof theory, highlighting both the constructive benefits and practical limitations. The discussion links interpolation to proof complexity and universal proof theory, offering a road map for building interpolation proofs in modern, modular proof systems and for extracting interpolants from proofs in contemporary calculi.

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.