subformula property (anchored proofs) 0
Hello,
I would like to ask for some explanation on some property of propositional sequent calculus. The sequent calculus that I use here follows that of Stephen Cook, in "Logical Foundations of Proof Complexity". A pdf draft of that book can be found at his website: http://www.cs.toronto.edu/~sacook/
Definition: A PK-proof $\pi$ of a sequent S from $\Phi$, where $\Phi$ is a set of sequents, is said to be anchored if every cut formula in $\pi$ occurs as a formula of some sequent in $\Phi$.
Proposition: If $\pi$ is an anchored PK-proof of a sequent S from $\Phi$, then every formula in every sequent of $\pi$ either occurs as a formula in some sequent in $\Phi$ or is a subformula of some formula in S.
The proof is supposed to be by induction on the number of sequents in $\pi$. However, I am stuck in the induction step. Could someone please help me as I would really like to understand that proof.
Thank you!
 A: It might help to explain what you're stuck on, since the proof in the book looks pretty clear to me, but I'll try to explain in a bit more detail.
In the inductive case, $\pi$ is the result of applying a rule to either one or two smaller proofs.  For simplicity, consider the case with one smaller proof, so $\pi$ is the result of applying some rule to some sequent $S'$, where there is a PK-proof $\pi'$ of $S'$ from $\Phi$ and $\pi'$ must have fewer sequents than $\pi$ did.
By the inductive hypothesis, it must be that every formula in every sequent of $\pi'$ either occurs as a formula in some sequent in $\Phi$ or is a subformula of some formula in $S'$.  Now consider some sequent $T$ of $\pi$; either this is the last sequent of $\pi$, in which case every formula in $T$ appears as a subformula (and indeed, a formula) of some formula in $S$, or $T$ is also in $\pi'$.  In the latter case, we already know that every formula in $T$ either occurs as a formula in some sequent in $\Phi$, or is a subformula of some formula in $S'$.  But every formula in $S'$ is a subformula of some formula in $S$---every rule besides the cut rule only builds up larger formulas, and therefore has this property.
The case where the rule had two premises is basically the same; we use the fact that the inductive hypothesis held for both premises.
In the case where the rule is the cut-rule, the statement is directly guaranteed by the anchored property.
