<p>Girard is talking about <em>intuitionistic</em> 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 <em>empty</em>. We can rewrite the cut rule as follows, writing $B^?$ for a sequence which is either empty or contains a single formula.</p>

<p>$$
\frac{\vec{A} \vdash C \qquad \vec{A&#39;},C \vdash B^?}
     {\vec{A}, \vec{A&#39;} \vdash B^?}
$$</p>

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

CC BY-SA 3.0
2011-10-22T22:10:25.037Z
I still do not understand. Are we applying the same criteria to decide the "stronger than" relation in both the identity and cut rules?
Kevin Clancy
CC BY-SA 3.0
2011-10-11T07:28:39.717Z
2011-10-11T07:28:39.717Z
Neel Krishnaswami
<p>On page 30 of "Proofs and Types" by Girard, Taylor, and Lafont, it is claimed that that the identity axiom for sequent calculus:</p>

<p>C ├ C</p>

<p>has a converse relation with the cut rule:</p>

<p>$$\frac{\vec{A} \vdash C,\vec{B}  \qquad \vec{A&#39;},C \vdash \vec{B&#39;}}
      {\vec{A},\vec{A&#39;} \vdash \vec{B},\vec{B&#39;}}$$</p>

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

<lo.logic><proof-theory><sequent-calculus>
converse relationship between the cut rule and the identity axiom
Kevin Clancy
# converse relationship between the cut rule and the identity axiom

(Asked by: username_0 on 2011-10-11)

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?

**Tags:** lo.logic, proof-theory, sequent-calculus

---

## 1 answers

### Answer by username_1 on 2011-10-11. Score: 5

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.

> **Comments:**
> **username_0**: I still do not understand. Are we applying the same criteria to decide the "stronger than" relation in both the identity and cut rules?  

---

