Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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!

share|improve this question

1 Answer 1

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.

share|improve this answer
    
Dear Henry, thank you for you answer. –  michael Feb 22 '12 at 19:09

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.