<p>I extend what I wrote as a comment. As there is a great number of cases in the proof, I only give an idea of why this transformation terminates. The short answer is:</p>

<p><strong>In the case promotion vs contraction, after the transformation, the number of contractions in the part of the proof containing cuts has decreased by one.</strong></p>

<p>To go a bit more into details, I would say that you were mistaken because you thought that either the number of cuts or the size of the proof should decrease in order to ensure termination. However, termination can be proven by looking at other parameters of the proof. </p>

<p>If you want to prove termination, you only have to show that each rule will be applied a finite number of time. You can prove that the transformation rule promotion vs contraction will be applied at most m times, where m is the number of contractions in your initial proof. To prove this, you just have to observe that no rule introduces a new contraction in proof tree. And this one decreases the number of contraction by one. You can do this trick for any other rules "promotion vs sthg" to prove that this one will be applied only a finite number of time.</p>

CC BY-SA 3.0
2017-01-22T15:19:13.593Z
2017-01-22T15:19:13.593Z
holf
<p>In Melliès’ survey <a href="https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/categorical-semantics-of-linear-logic.pdf">Categorical Semantics of Linear Logic</a>, a cut elimination procedure for intuitionistic linear logic is given which includes the following case:</p>

<blockquote>
<h3>3.9.3 Promotion vs. contraction</h3>
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}
$$
</blockquote>

<p>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.</p>

CC BY-SA 3.0
2017-01-20T10:53:37.957Z
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
CC BY-SA 3.0
2017-01-20T11:11:33.743Z
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
CC BY-SA 3.0
2017-01-20T12:05:29.123Z
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
CC BY-SA 3.0
2017-01-20T17:12:37.280Z
I just looked at the notes, and agree with @holf -- this is the only step that changes the number of contractions. But if you want a more obviously inductive proof, then look at Pfenning's paper *Structural Cut Elimination in Linear Logic* (this is for classical LL, but the same arguments works for the intuitionistic case) .
Neel Krishnaswami
CC BY-SA 3.0
2017-01-20T18:42:43.267Z
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
CC BY-SA 3.0
2017-01-20T19:33:52.747Z
@NeelKrishnaswami: Thanks. I've seen that paper, and I remember you also used a dyadic presentation in your MGS lectures last year. I'm asking because I also want to understand the proof for the monadic presentation.
Sebastien Zany
CC BY-SA 3.0
2017-06-16T17:26:18.023Z
I have to disagree with holf's answer, in the sense that I do not see why the argument works. Counting the number of contractions above the cut works only if no reduction creates new contractions, but not only above the new cuts: below too! But this "Series of Contractions and Exchanges" in the reduction is a problem. By doing this step, you create two new cuts: A (above) and B (below). Now, say that you eliminate A (which is possible by induction because it has lesser rank and less contractions above it). How do you know that eliminating it does not increase the number of contractions above B
Jérôme Fortier
CC BY-SA 3.0
2017-06-16T17:37:33.917Z
Isn't it ok because you eliminate the $B$-cut before you eliminate the $A$-cut?
Max New
CC BY-SA 3.0
2017-06-19T14:13:17.167Z
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
<linear-logic>
Why does this cut elimination procedure terminate (contraction case)?
Sebastien Zany
# Why does this cut elimination procedure terminate (contraction case)?

(Asked by: username_0 on 2017-01-20)

In Melliès’ survey [Categorical Semantics of Linear Logic](https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/categorical-semantics-of-linear-logic.pdf), 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.

**Tags:** linear-logic
> **Comments:**
> **username_1**: 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.  
> **username_0**: 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.)  
> **username_1**: 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.  
> **username_2**: I just looked at the notes, and agree with @holf -- this is the only step that changes the number of contractions. But if you want a more obviously inductive proof, then look at Pfenning's paper *Structural Cut Elimination in Linear Logic* (this is for classical LL, but the same arguments works for the intuitionistic case) .  
> **username_3**: 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)  
> **username_0**: @NeelKrishnaswami: Thanks. I've seen that paper, and I remember you also used a dyadic presentation in your MGS lectures last year. I'm asking because I also want to understand the proof for the monadic presentation.  
> **username_4**: I have to disagree with holf's answer, in the sense that I do not see why the argument works. Counting the number of contractions above the cut works only if no reduction creates new contractions, but not only above the new cuts: below too! But this "Series of Contractions and Exchanges" in the reduction is a problem. By doing this step, you create two new cuts: A (above) and B (below). Now, say that you eliminate A (which is possible by induction because it has lesser rank and less contractions above it). How do you know that eliminating it does not increase the number of contractions above B  
> **username_5**: Isn't it ok because you eliminate the $B$-cut before you eliminate the $A$-cut?  
> **username_4**: 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.  

---

## 1 answers

### Answer by username_1 on 2017-01-22. Score: 4

I extend what I wrote as a comment. As there is a great number of cases in the proof, I only give an idea of why this transformation terminates. The short answer is:

**In the case promotion vs contraction, after the transformation, the number of contractions in the part of the proof containing cuts has decreased by one.**

To go a bit more into details, I would say that you were mistaken because you thought that either the number of cuts or the size of the proof should decrease in order to ensure termination. However, termination can be proven by looking at other parameters of the proof.

If you want to prove termination, you only have to show that each rule will be applied a finite number of time. You can prove that the transformation rule promotion vs contraction will be applied at most m times, where m is the number of contractions in your initial proof. To prove this, you just have to observe that no rule introduces a new contraction in proof tree. And this one decreases the number of contraction by one. You can do this trick for any other rules "promotion vs sthg" to prove that this one will be applied only a finite number of time.


---

