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.

1. 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.
2. Pudlák, Pavel. Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic 62.3 (1997): 981-998.