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?


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.

  • $\begingroup$ I still do not understand. Are we applying the same criteria to decide the "stronger than" relation in both the identity and cut rules? $\endgroup$ – Kevin Clancy Oct 22 '11 at 22:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.