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

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