# subformula property (anchored proofs)

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!

-
I think this is more suitable for MSE. –  Kaveh Feb 22 '12 at 1:07
Kaveh, are you confident there will be people at math.se with the necessary expertise to answer this question? (This is an honest question -- I don't know the answer because I don't spend much time there. But we have recently discussed on meta the issue of being too ready to direct people to math.se.) –  Todd Trimble Feb 22 '12 at 1:32
@Todd, it is definitely not research level and there are people on MSE that can answer it. If you read the definitions and look at the rules you will see why this should be true. We teach this in undergraduate logic courses (anchored is more or less the same as free-cut free). –  Kaveh Feb 22 '12 at 2:04
Kaveh -- just making sure. I know it's not research level. –  Todd Trimble Feb 22 '12 at 4:04