Inversion lemma proof

Question

I am following Structural Proof Theory by Negri and others, and I don't understand the Inversion Lemma proof (i) (the system is G3$_{ip}$, which is the same as G3$_i$ only that it excludes quantifier rules):

a) How can $A\land B, \Gamma \Rightarrow C $ be an axiom? I thought the whole point of G3$_{ip}$/G3$_i$ is that the RHS in axiom rules can only be atomic (ie $P, \Gamma \Rightarrow P$ where P is atomic)? Is the author saying the base case is vacuously true if $A\land B, \Gamma \Rightarrow C $ is an axiom?

I also don't understand how it has been concluded that $A, B, \Gamma \Rightarrow C$ is an axiom or conclusion of $L\bot$.

b) In the case where $A\land B$ is principal, I get how $\vdash_n A, B, \Gamma \Rightarrow C$ - but shouldn't the conclusion be $\vdash_{n+1} A, B, \Gamma \Rightarrow C$ instead?

c) In the case where it is not principal, when it talks about 'applying the last rule', is it saying: since we know the last rule is not L$\land$, so $A$ and $B$ are definitely not acted upon. So let the last rule acts upon $\Gamma^{'}$/$\Gamma^{"}$ and $C{'}$/$C{''}$, and let the product be $\Gamma$ and $C$. Since we are at depth $n+1$, we get $\vdash_{n+1} A, B, \Gamma \Rightarrow C$?

(I am aware of a similar question Inversion lemma for G3ip, but this question does not seem to concern mine directly)

Answer 1

Any instance of the axiom rule has the form $P, \Gamma \Rightarrow P$, where $P$ is an atomic formula and $\Gamma$ is a finite multiset of formulas. Possibly, $\Gamma$ contains a formula $A \land B$ or whatever formula you like.

Moreover, the notation $\vdash_n \Gamma \Rightarrow C$ means that there exists a derivation with conclusion $\Gamma \Rightarrow C$ and heigth at most$-$possibly not exactly$-\!n$ (see p. 31 in the text you cited: Structural Proof Theory by Negri and von Plato).

1. If $A \land B, \Gamma \Rightarrow C$ is an axiom, then $C = P \in \Gamma$ for some atomic formula $P$ and clearly $\vdash_0 A \land B, \Gamma \Rightarrow P$. Then, $\vdash_0 A, B, \Gamma \vdash P$ because $A, B, \Gamma \vdash P$ is another instance of the axiom.

   If $A \land B, \Gamma \Rightarrow C$ is the conclusion of $L\bot$, then $\bot \in \Gamma$ and clearly $\vdash_0 A \land B, \Gamma \Rightarrow C$. Then, $\vdash_0 A, B, \Gamma \vdash C$ because $A, B, \Gamma \vdash C$ is another instance of the rule $L\bot$.

2. If $A \land B$ is principal, then the derivation $\Phi$ has the form \begin{align} \dfrac{\overset{\vdots \Phi'}{A, B, \Gamma \Rightarrow C}}{A \land B, \Gamma \Rightarrow C}L\land \end{align} where $h(\Phi) = h(\Phi') + 1$ ($h(\Phi)$ stands for the height of the derivation $\Phi$). So, $ \vdash_{h(\Phi)} A \land B, \Gamma \Rightarrow C$, which implies that $ \vdash_{h(\Phi)} A, B, \Gamma \Rightarrow C$ because in general $\vdash_{n} \Gamma \Rightarrow C$ means that there exists a derivation whose height is at most $n$ (see p. 31).

3. If $A \land B$ is not principal, then the derivation $\Phi$ has the form (I consider only the binary case for the last rule, the case where the last rule is unary is analogous) \begin{align} \dfrac{\overset{\vdots \Phi'}{A \land B, \Gamma' \Rightarrow C'} \qquad \overset{\vdots \Phi''}{A \land B, \Gamma'' \Rightarrow C''}}{A \land B, \Gamma \Rightarrow C}\diamond \end{align} where $h(\Phi) = h(\Phi') + h(\Phi'') + 1$. By induction hypothesis (since $h(\Phi') < h(\Phi)$ and $h(\Phi'') < h(\Phi)$), one has $ \vdash_{h(\Phi')} A, B, \Gamma' \Rightarrow C'$ and $ \vdash_{h(\Phi'')} A, B, \Gamma'' \Rightarrow C''$. By applying the rule $\diamond$ to the conclusions $A, B, \Gamma' \Rightarrow C'$ and $A, B, \Gamma'' \Rightarrow C''$, you get a derivation of $A,B, \Gamma \Rightarrow C$ whose height is at most $h(\Phi') + h(\Phi'') + 1$. Therefore, $ \vdash_{h(\Phi)} A, B, \Gamma \Rightarrow C$.