proof-theoretic proof of Craig's interpolation theorem

251 Views Asked by At

I am approaching the Craig's interpolation theorem from a proof-theoretic point of view. In particular I am trying to give a proof of the statement using the sequent calculus (both in the intuitionistic and classical case), via induction on the complexity of the derivation. However I am stuck at the case in which the last rule of the derivation is an introduction of implication to the left. Does anyone please know where I can take some inspiration? Some paper, article or book to consult? or of course, has anyone ever tackle this proof?