Exchange case in proving interpolation theorem by induction on the length of proof tree

Question

I'm trying to prove Craig's interpolation theorem of propositional logic using Maehara's method by induction on the length of proof tree using sequent calculus. the theorem is as stated below: $$ \forall \Gamma_1 \Gamma_2 \Delta_1 \Delta_2: \Gamma_1,\Gamma_2 \vdash \Delta_1,\Delta_2 $$ $$ \rightarrow \exists c: \Gamma_1 \vdash c,\Delta_1 \land c,\Gamma_2 \vdash \Delta_2$$ $$\land (atomsof(c) \subseteq atomsof(\Gamma_1,\Delta_1) \cap atomsof(\Gamma_2,\Delta_2))$$ and here I'm stuck in the case where the proof ends by exchange rule like this: $$ \frac{\Gamma_1,\Gamma_2 \vdash \Delta,a,b,\Delta'}{\Gamma_1,\Gamma_2 \vdash \Delta,b,a,\Delta'}$$ Here in induction hypotheses we have $$ \forall \Delta_1' \Delta_2': \Delta,a,b,\Delta' = \Delta_1',\Delta_2' $$ $$ \rightarrow \exists c': \Gamma_1 \vdash c',\Delta_1' \land c',\Gamma_2 \vdash \Delta_2'$$ $$\land (atomsof(c) \subseteq atomsof(\Gamma_1,\Delta_1') \cap atomsof(\Gamma_2,\Delta_2'))$$ and we have to deduce that $$ \forall \Delta_1 \Delta_2: \Delta,b,a,\Delta' = \Delta_1,\Delta_2 $$ $$ \rightarrow \exists c: \Gamma_1 \vdash c,\Delta_1 \land c,\Gamma_2 \vdash \Delta_2$$ $$\land (atomsof(c) \subseteq atomsof(\Gamma_1,\Delta_1) \cap atomsof(\Gamma_2,\Delta_2))$$ I'm stuck with the case where $\Delta_1 = \Delta,b $ and $ \Delta_2 = a,\Delta'$, I can't find the desired interpolant here, I couldn't find the original paper which is by the way written in Japanese. also I couldn't find the complete proof anywhere the closest I got was in "Proof Theory and logical complexity" by Jean-Yves Girard which even there he didn't cover exchange rule.

Answer 1

In order to prove Craig's interpolation theorem for propositional logic using Maehara's method, I would propose to modify the calculus. Consider a similar calculus, where the left and right parts of sequents are finite multisets (instead of finite sequences). This modified calculus does not have explicit exchange rules. First, one can prove that the modified calculus is equivalent to the original one. After that, one can prove the theorem as you stated it (by induction).

Another approach would be to use finite sequences, but modify the claim that we prove by induction. We would need to consider sequents of the form $\Gamma_1^1,\Gamma_2^1,\Gamma_1^2,\Gamma_2^2,\ldots,\Gamma_1^k,\Gamma_2^k \vdash \Delta_1^1,\Delta_2^1,\Delta_1^2,\Delta_2^2,\ldots,\Delta_1^k,\Delta_2^k$ and construct an interpolant $c$ such that $\Gamma_1^1,\Gamma_1^2,\ldots,\Gamma_1^k \vdash c,\Delta_1^1,\Delta_1^2,\ldots,\Delta_1^k$ and $c,\Gamma_2^1,\Gamma_2^2,\ldots,\Gamma_2^k \vdash \Delta_2^1,\Delta_2^2,\ldots,\Delta_2^k$. The induction would be over proof length, as usual.