Speaker
Alexis Saurin
IRIF, CNRS
Talks at this conference:
Friday, 14:00, J335 
CraigLyndon interpolation as cutintroduction 
After Craig’s seminal results on interpolation theorem [1], a number and variety of prooftechniques, be they semantical or prooftheoretical, 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 cutfree complete proof systems. We reconsider here Maehara’s method and show how, by a close inspection of the proof, one can extract a “proofrelevant” interpolation theorem for firstorder linearlogic stated as follows: if \(\pi\) is a cutfree 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\) cutreduces \(\pi\). We then show that this can be decomposed in two phases: (i) a bottomup 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 proofrelevant 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
