Interpolation through the lens of proof theory Lecture notes for Logic Summer School @ANU 2024, Canberra, Australia

Craig interpolation is a fundamental concept in mathematical logic and computer science. Craig interpolants are formulas in a specified vocabulary that, intuitively speaking, explain why one formula entails the other. The existence of Craig interpolants is a useful property serving in many applications. For example, in knowledge representation, interpolants are used to enlarge knowledge bases by learning new concepts. In proof complexity, the feasible extraction of interpolants from proofs relates to the NP vs co-NP problem.

The goal of the course is to introduce theory and practice of interpolation through the lens of proof theory. Proof theoretic techniques allow to explicitly construct interpolants which is useful in computations. We will discuss methods based on sequent calculi. We will discuss uniform interpolation, a strengthening of Craig’s interpolation. We illustrate the applications of interpolation in the fields of universal proof theory, knowledge representation, and proof complexity.