Interestingly there is a connection between cut-elimination and the interpolation theorem. First of all the interpolation theorem looks like a reverse of the mix rule elimination used during cut-elimination. This elimination says:
If G |- A and D, A |- B are cut-free proofs,
then there is a cut-free proof G, D |- B
Now one form of interpolation theorem based on cut-free proofs, can be done as follows. Its the upside down version of the elimination. It starts with G, D |- B and gives G |- A and D, A |- B:
If G; D |- B is a cut free proof,
then there is a formula A (the interpolant)
and cut free proofs G |- A and D, A |- B,
and A uses only propositions simultaneously from G and D
I put on purpose a semicolon between the premisses G and D. This is where we draw the line, which premisses we want to see as delivering the interpolant, and which premisses we want to see using the interpolant.
When the input is a cut free proof, the effort of the algroithm is proportional
to the number of nodes of the cut free proof. So its practical a method linear
in the input. With each proof step of the cut free proof, the algorithm assembles
the interpolant by introducing a new connective.
The above observation holds for the simple interpolation construction, where
we only require that the interpolant has propositions simultaneously from G
and D. Interpolants with a variable condition require a little bit more steps,
since some variable hinding needs also to be done.
Probably there is a connection between the minimality of the cut-free proof and
the size of the interpolant. Not all cut-free proofs are minimal. For example
uniform proofs are often shorter than cut-free proofs. The lemma for uniform
proofs is quite simple, a rule application of the form:
G |- A G, B |- C
G, A -> B |- C
Can be avoided, when B is not used in the proof of C. When B is not used in
the proof of C, we have already G |- C, and thus by weakening G, A -> B |- C.
The interpolation algorithm mentioned here, will not pay attention on this.
Craig’s Interpolation Theorem formalised and mechanised in Isabelle/HOL,
Tom Ridge, University of Cambridge, 12 Jul 2006
The above refence does not exactly show the same interpolation, since
it uses multi-sets in the conclusion part of a sequent. Also it does not
make use of implication. But it is interesting since it supports my complexity
claim, and since it shows a mechanized verification.