# On the Completeness of Interpolation Procedures

## Abstract#

Craig interpolation is a fundamental property of logic. Suppose a calculus G for propositional logic (for instance the propositional LK) and an interpolation procedure I (for example, the Maehara-style interpolation procedure) are given. We are interested in the power of the interpolation procedure with respect to the calculus. Stating the problem precisely: Let C be a (semantically possible) interpolant for a given tautology A->B. Does there exist a proof π of A->B such that I(π)=C? A positive answer to the question allows us to call the interpolation procedure I complete for G. If we take G to be the cut-free propositional LK, then the standard Maehara-style interpolation (call it M) fails to provide a positive answer to the question. Similarly, for propositional resolution and the standard algorithm to find the interpolant as considered by Krajíček and Pudlák [1, 2]. However, if we take G to be the propositional LK with atomic cuts, then M is complete for G. This shows that to construct any possible interpolant via the Maehara-style interpolation procedure, using the cut rule is inevitable.

What if we move to the realm of first-order logic? Then, obviously, M is incomplete for the cut-free first-order LK. Interestingly though, M for first-order LK with atomic cuts is also incomplete. This talk is based on an ongoing research with Stefan Hetzl.

- Krajíček, Jan.
*Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic.*The Journal of Symbolic Logic 62.2 (1997): 457-486. - Pudlák, Pavel.
*Lower bounds for resolution and cutting plane proofs and monotone computations.*The Journal of Symbolic Logic 62.3 (1997): 981-998.