Explanation on the symmetry between identity axiom and cut rule

Question

In Proofs And Types at the beginning of 5.1.4 Girard says that the identity axiom is somewhat complementary to the cut rule, more specifically 'The identity axiom says that $C$ (on the left) is stronger than $C$ (on the right); this [cut] rule states the converse truth, i.e. $C$ (on the right) is stronger than $C$ (on the left).'

Can someone explain this to me a little bit further? I only vaguely get the first part of the statement, that the identity axiom roughly says that $C$ (on the left) implies $C$ (on the right), but I don't know what to make of the second part.

Answer 1

I'll add a "long comment" to fweth's one ...

Consider the rules for $\to$ (the conditional). They are respectively :

$$(\to \text {-left)} \ \ \frac{\Gamma \vdash \Delta, C \quad D \vdash \Pi, \Lambda}{C \to D, \Gamma, \Pi \vdash \Delta, \Lambda}$$

and

$$(\to \text {-right)} \ \ \frac{C, \Gamma \vdash \Delta, D}{\Gamma \vdash \Delta, C \to D}.$$

Omitting the contexts and replacing $D$ with $C$, they look like :

$$(\to \text {-left)} \ \ \frac{ \vdash C \quad C \vdash }{C \to C \vdash }$$

and

$$(\to \text {-right)} \ \ \frac{C \vdash C}{\vdash C \to C}.$$

Now, we can "read" them as meaning respectively :

• the axiom rule licences the derivation of the tautological : $C \to C$,

while :

• the cut rule licences us to "discard" the contradictory : $\lnot (C \to C)$.

Answer 2

I think he means that if we chose all sequences in the cut rule $$\frac{\underline{A}\vdash C,B\quad\underline{A}',C\vdash\underline{B'}}{\underline{A},\underline{A}'\vdash\underline{B},\underline{B}'}$$ to be empty, then we can informally read it as '($\vdash C$ a.k.a. $C$-on-the-right) and ($C\vdash$ a.k.a. not $C$-on-the-left) implies ($\vdash$ a.k.a. contradiction)', hence $C$ on the right implies $C$ on the left.