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!