subformula property (anchored proofs)

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!

-

1 Answer

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.

-
Dear Henry, thank you for you answer. – michael Feb 22 '12 at 19:09