converse relationship between the cut rule and the identity axiom

Question

On page 30 of "Proofs and Types" by Girard, Taylor, and Lafont, it is claimed that that the identity axiom for sequent calculus:

C ├ C

has a converse relation with the cut rule:

$$\frac{\vec{A} \vdash C,\vec{B} \qquad \vec{A'},C \vdash \vec{B'}} {\vec{A},\vec{A'} \vdash \vec{B},\vec{B'}}$$

The explanation it gives is that the in the identity axiom, C on the left is stronger than C on the right. With the cut rule, it claims, C on the right is stronger than C on the left. While the claim about the identity axiom seems to follow from basic notions of sequents, I do not understand the claim about the cut rule. Could someone explain this?

Answer 1

Girard is talking about intuitionistic sequents, in which sequences to the right of the turnstile have length at most 1. So in the premiss of the cut rule, the sequence of formulas $\vec{B}$ is empty. We can rewrite the cut rule as follows, writing $B^?$ for a sequence which is either empty or contains a single formula.

$$ \frac{\vec{A} \vdash C \qquad \vec{A'},C \vdash B^?} {\vec{A}, \vec{A'} \vdash B^?} $$

Now, it's easy to see why Girard says $C$ on the right is stronger -- it is the only formula that occurs to the right in the first premiss.