Interpolation in Proof Theory

TL;DR

This chapter reviews proof-theoretic techniques for establishing interpolation properties in various logics, emphasizing constructive and modular methods that connect proof systems with interpolation results.

Contribution

It synthesizes foundational methods like Maehara's and Pitts' for interpolation, highlighting their role in modern proof theory and providing a roadmap for constructing interpolation proofs.

Findings

Demonstrates how proof-theoretic methods establish interpolation properties.

Shows the connection between proof systems and interpolation results.

Provides a constructive approach to interpolation in diverse logics.

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.