On the Completeness of Interpolation Algorithms
Stefan Hetzl, Raheleh Jalali
TL;DR
The paper introduces a precise notion of semantic completeness for interpolation algorithms and systematically analyzes this property across resolution, sequent calculi, modal logics, and first-order logic. It proves strong incompleteness results for standard, cut-free interpolation algorithms in propositional settings, but shows completeness can be recovered under refinements such as pruning/subsumption and, crucially, atomic cuts in the sequent calculus. The modal extensions preserve the completeness results under the atomic-cut framework, while the first-order case reveals inherent limitations in the common two-phase strategies for interpolant construction, with Beth definability tied to these completeness properties. Overall, the work clarifies how proof-system freedom and algorithmic strategies interact to determine the expressive reach of interpolation procedures, and it lays groundwork for further exploration in local proofs, FO logics, and intuitionistic variants.
Abstract
Craig interpolation is a fundamental property of classical and non-classic logics with a plethora of applications from philosophical logic to computer-aided verification. The question of which interpolants can be obtained from an interpolation algorithm is of profound importance. Motivated by this question, we initiate the study of completeness properties of interpolation algorithms. An interpolation algorithm $\mathcal{I}$ is \emph{complete} if, for every semantically possible interpolant $C$ of an implication $A \to B$, there is a proof $P$ of $A \to B$ such that $C$ is logically equivalent to $\mathcal{I}(P)$. We establish incompleteness and different kinds of completeness results for several standard algorithms for resolution and the sequent calculus for propositional, modal, and first-order logic.