Interpolation in First-Order Logic
Balder ten Cate, Jesse Comer
TL;DR
This chapter provides a comprehensive overview of Craig interpolation for $FO$ and its decidable fragments, detailing foundational theorems (Craig, Lyndon, Otto, access), refinements, and fundamental negative results. It surveys a broad range of applications, from definability and preservation theorems to knowledge-base merging and formal verification, and connects interpolation to $ exists$SO/$\forall$SO definability through $\Delta$-interpolation. The decidable-fragment landscape is mapped (e.g., $FO^2$, $GFO$, $UNFO$, $GNFO$, $C_2$, $FF$, $FL$, $AF$) with results on CIP, repair strategies, and tight complexity bounds, highlighting the trade-offs between expressivity and interpolability. The chapter also covers interpolation relative to theories, algorithmic aspects, and constructive proof methods (notably semantic tableaux) for extracting interpolants, while noting open questions such as the existence of uniform interpolants and the limits of CIP in various logics.
Abstract
In this chapter we give a basic overview of known results regarding Craig interpolation for first-order logic as well as for fragments of first-order logic. Our aim is to provide an entry point into the literature on interpolation theorems for first-order logic and fragments of first-order logic, and their applications. In particular, we cover a range of known refinements of the Craig interpolation theorem, we discuss several important applications of interpolation in logic and computer science, we review known results about interpolation for important syntactic fragments of first-order logic, and we discuss the problem of computing interpolants.