1
$\begingroup$

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 Answers 1

2

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.

  • 0
    Dear Henry, thank you for you answer.2012-02-22