# Why does this cut elimination procedure terminate (contraction case)?

In Melliès’ survey Categorical Semantics of Linear Logic, a cut elimination procedure for intuitionistic linear logic is given which includes the following case:

### 3.9.3 Promotion vs. contraction

The proof $$\displaystyle\frac{ \displaystyle\frac{\displaystyle\frac{\pi_1\\\vdots}{!\Gamma \vdash A}}{!\Gamma \vdash !A} \text{ Promotion} \qquad \displaystyle\frac{\displaystyle\frac{\pi_2\\\vdots}{\Upsilon_1 , !A , !A , \Upsilon_2 \vdash B}}{\Upsilon_1 , !A , \Upsilon_2 \vdash B} \text{ Contraction} }{ \Upsilon_1 , !\Gamma , \Upsilon_2 \vdash B } \text{ Cut}$$ is transformed into the proof $$\displaystyle\frac{ \displaystyle\frac{\displaystyle\frac{\pi_1\\\vdots}{!\Gamma \vdash A}}{!\Gamma \vdash !A} \text{ Promotion} \qquad \displaystyle\frac{ \displaystyle\frac{\displaystyle\frac{\pi_1\\\vdots}{!\Gamma \vdash A}}{!\Gamma \vdash !A} \text{ Promotion} \qquad \displaystyle\frac{\pi_2\\\vdots}{\Upsilon_1 , !A , !A , \Upsilon_2 \vdash B} }{ \Upsilon_1 , !A , !\Gamma , \Upsilon_2 \vdash B } \text{ Cut} }{ \displaystyle\frac{\Upsilon_1 , !\Gamma , !\Gamma , \Upsilon_2 \vdash B}{\Upsilon_1 , !\Gamma , \Upsilon_2 \vdash B} \rlap{\;\text{ Series of Contractions and Exchanges}} } \text{ Cut}$$

Why is this a valid inductive step? Neither the size of the cut formula nor the sizes of the derivations are decreasing. (In the transformed proof, the right branch of the lower cut is potentially larger after inductively eliminating the upper cut.) So it's not clear why this procedure should terminate.

• Just had a quick look and this is a long time since I haven't read such formalism but I got the impression that the goal here is to remove the cut after a Promotion vs Contraction. In this case, the transformation works as every contraction is now under the cut so the cuts goes up in the derivation tree and are inductively eliminated. – holf Jan 20 '17 at 10:53
• The problem is that in the transformed proof, the right branch of the lower cut is potentially larger after inductively eliminating the upper cut. (Will add this in clarification.) – Sebastien Zany Jan 20 '17 at 11:11
• Yes, but the number of contractions have been reduced by one. As far as I can tell (again, I did not go too much into details), no other transformations increase the number of contractions. So if you look at the value (#contraction, whatever_you_need_for_the_rest), then this value always decreases in the lexicographical order, so it will terminates at some point. – holf Jan 20 '17 at 12:05
• Besides what holf and Neel said, doesn't a variation of the usual (degree,rank) argument work? I mean, what's the difference between this step and the usual elimination of a cut on a contraction in LJ? (I mean Gentzen's intuitionistic sequent calculus) – Damiano Mazza Jan 20 '17 at 18:42
• But how do you eliminate the cut B? The only thing it seems you can do in the Promotion-Cut case is to swap the positions of the two cuts A and B. But then, you end up in the exact same situation. If you eliminate B (which is now above), you may increase the number of contractions above A. – Jérôme Fortier Jun 19 '17 at 14:13