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!