Welcome to MathOverflow

Question

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!

flag	asked Feb 21 2012 at 23:55 michael 1

1

I think this is more suitable for [MSE](mathematics.stackexchange.com). – Kaveh Feb 22 2012 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 2012 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 2012 at 2:04

Kaveh -- just making sure. I know it's not research level. – Todd Trimble Feb 22 2012 at 4:04

subformula property (anchored proofs)

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.