# Craig-Lyndon interpolation as cut-introduction

## Alexis Saurin

After Craig’s seminal results on interpolation theorem [1], a number and variety of proof-techniques, be they semantical or proof-theoretical, have been designed to prove interpolation theorems. Among them, Maheara’s method [3] is specific due to its wide applicability to a range of logics admitting cut-free complete proof systems.

We reconsider here Maehara’s method and show how, by a close inspection of the proof, one can extract a “proof-relevant” interpolation theorem for first-order linear-logic stated as follows: if \(\pi\) is a cut-free proof of \(A \vdash B\), we can find (i) a formula \(C\) in the common vocabulary of \(A\) and \(B\) and (ii) proofs \(\pi_1\) of \(A \vdash C\) and \(\pi_2\) of \(C \vdash B\) the proof \(\pi'\) obtained from \(\pi_1\) and \(\pi_2\) with a cut inference on \(C\) cut-reduces \(\pi\).

We then show that this can be decomposed in two phases: (i) a bottom-up phase which decorates the sequents followed by (ii) a top down phase which solves the interpolation problem, *synthesizing the interpolant by introducing cuts*.

We then consider extensions of the approach to other settings (classical and intuitionistic logics, or the \(\mu\)-calculus) and discuss the computational content of the result which is related to a proof-relevant refinement of Prawitz’ proof of the interpolation theorem [4] in natural deduction already investigated by Čubrić in the 90’s [2] for the simply typed \(\lambda\)-calculus.

Details are provided in an extended version [5].

## Bibliography

- William Craig,
*Three uses of the Herbrand-Gentzen theorem in relating model theory andproof theory*,,vol. 22(3) (1957), pp. 269–285.*Journal of Symbolic Logic* - Djordje Čubrić,
*Results in categorical proof theory*,,1993.*PhD thesis, McGill University* - Shoji Maehara,
*On the interpolation theorem of Craig*,, vol 12(4) 1960.*Sûgaku* - Dag Prawitz,
,Dover Publications, Mineola, N.Y., 1965.*Natural Deduction: A Proof-Theoretical Study* - Alexis Saurin,
,draft, 2024, www.irif.fr/_media/users/saurin/pub/interpolation_as_cut_introduction.pdf*Interpolation as cut introduction*