Inversion lemma for G3ip

Question

I'm following the book Structural Proof Theory by Negri and others.

In it, they claim on page 32 about G3ip that if $⊢ _ n A \& B, Γ ⇒ C$, then $⊢ _ n A, B, Γ ⇒ C$.

But, given that the only derivation of $P _ 1 \& P _ 2 ⇒ P _ 1$ has height 1, how can you possibly get a derivation of $P _ 1, P _ 2 ⇒ P _ 1$ also of height 1.

If the lemma is wrong, how do you correct it?

Answer 1

The Lemma is not wrong...

A derivation of height 1 in sequent calculus is a single application of one of the rules [see page 28], like :

$$\frac{A, B, \Gamma \Rightarrow C}{A \& B, \Gamma ⇒ C} \, L\&.$$

If so, what is "a derivation of $P_1 \& P_2 ⇒ P_1$" ?

It must be :

$$\frac{P_1, P_2 \Rightarrow P_1}{P_1 \& P_2 ⇒ P_1},$$

where the upper sequent, is a Logical axiom : $P_1, \Gamma \Rightarrow P_1$.

The height of a derivation [see page 30] is :

the greatest number of successive applications of rules in it, where an axiom and $L \bot$ have height $0$.

Thus the sequent : $P_1, P_2 \Rightarrow P_1$ is an axiom, and is derivable with height $0$ (and so also with height $1$ ...).