6
$\begingroup$

I saw this site saying weakening is a structural rule where the hypotheses or conclusion of a sequent may be extended with additional members and that contraction is a rule where two equal (or unifiable) members on the same side of a sequent may be replaced by a single member (or common instance). However, I can't seem to get the terms yet. There are even these symbols that looks like a T turned counterclockwise.

In simple terms, what are weakening and contraction? Can they even be described without the symbol that looks like a T turned counterclockwise?

$\endgroup$
  • 1
    $\begingroup$ The "T turned clockwise" means that whatever is on the right of that symbol can be proven using whatever is on the left of it. $\endgroup$ – 5xum Sep 16 '14 at 5:48
  • $\begingroup$ @5xum Great! The symbols look readable now. Are the tags on my question correct? :-D $\endgroup$ – Tamad Lang Sep 16 '14 at 5:51
  • 1
    $\begingroup$ Are you aware that you are taling about Sequent calculus ( en.wikipedia.org/wiki/Sequent_calculus) not the more well known Natural deduction ( en.wikipedia.org/wiki/Natural_deduction ) in natural deduction the structural rules are assumed "build in in the rules" the left rules are true whatever the right rules RW is or introduction , Rc is removing of duplicates. Sequent calculus is rather advanced, better start with natural deduction (but you will learn some bad habids on the way, so maybe it is no such good idea) , $\endgroup$ – Willemien Sep 16 '14 at 11:12
  • $\begingroup$ @Willemien Initially I had no idea. Thanks. $\endgroup$ – Tamad Lang Sep 17 '14 at 0:08
8
$\begingroup$

In sequent calculus, Weakening (or Thinning) and Contraction are the so-called structural rules of inference.

Weakening rule introduces an extra formula $D$ in the antecedent: :

$$\frac{\Gamma\vdash \Delta}{D,\Gamma\vdash \Delta} \text {LW}$$

or in the succedent :

$$\frac{\Gamma\vdash \Delta}{\Gamma\vdash \Delta,D} \text {RW}$$

of the sequent $\Gamma \vdash \Delta$, where $\Gamma, \Delta$ are sets of formulae.

The "meaning" of the rule is the following :

if we have a derivation of the sequent $\Gamma \vdash \Delta$, we can "add" a formula $D$ to the set of assumptions .

Contraction rule is :

$$\frac{D,D,\Gamma\vdash \Delta}{D,\Gamma\vdash \Delta} \text {LC}$$

and :

$$\frac{\Gamma\vdash \Delta,D,D}{\Gamma\vdash \Delta,D} \text {RC}$$

The "meaning" of the rule is the following :

we can always "cancel" redundant occurrences of a formula in the antecedent or succedent of a sequent.


Added

The basic semantic definitions for sequents are :

a sequent $\Gamma \vdash \Delta$ is satisfied in an interpretation if either some formula in $\Gamma$ is not satisfied, or some formula in $\Delta$ is satisfied

and :

a sequent is valid if it is satisfied in every interpretation.

This means that we have to "read" a sequent as follows :

$$(\gamma_1 \land \ldots \gamma_n) \rightarrow (\delta_1 \lor \ldots \delta_m)$$

where $\Gamma = \{ \gamma_1, \ldots, \gamma_n \}$ and $\Delta = \{ \delta_1, \ldots, \delta_m \}$.

For simplicity, assume that $\Gamma = \{ \gamma_1, \gamma_2 \}$ and $\Delta = \{ \delta_1, \delta_2 \}$.

The semantic definition above says that the sequent is valid iff, for every interpretation, either some formula in the antecedent is false or some formula in the succedent is true, i.e. :

$$\vDash (\gamma_1 \land \gamma_2) \rightarrow (\delta_1 \lor \delta_2)$$

If it so, then we can add a formula $D$ whatever to the antecedent, and if the conjunction $\gamma_1 \land \gamma_2$ is false the new conjunction $(\gamma_1 \land \gamma_2) \land D$ will still be false or we can add a formula $D$ whatever to the succedent, and if the disjunction $\delta_1 \lor \delta_2$ is true the new disjunction $(\delta_1 \lor \delta_2) \lor D$ will still be true.

In both cases, if the upper sequent $\Gamma \vdash \Delta$ is valid, then also the lower ones : $D,\Gamma \vdash \Delta$ and $\Gamma \vdash \Delta,D$ are.

$\endgroup$
  • $\begingroup$ I understand some parts of your answer now, thanks to @5xum. I just have a follow up question: Why is it that we can add a formula to the succedent? Wouldn't it mean that \Gamma can prove both \Delta and D now (which doesn't seem valid because of D)? $\endgroup$ – Tamad Lang Sep 16 '14 at 8:41
  • $\begingroup$ This is a wee bit late, but the succedent is a disjunctive list of predicates. $\Gamma\vdash \Delta, D$ means that at least one from predicate $D$ or the predicates in $\Delta$ can be derived from all from the predicates in $\Gamma$. @BernardPollo $\endgroup$ – Graham Kemp May 7 '18 at 10:05
1
$\begingroup$

Given statements p and q, where p proves q, weakening means we can add any number of statements r to the left using conjunction (and, &), yet "p & r proves q" is still valid. This is the case because we know that we can prove q if p is true, and we can prove p if "p & r" is true (using conjunction elimination, or subtraction). Therefore, we can prove q if "p & r" is true, no matter what r is.

Contraction means we can add any number of statements r to the left using disjunction (or, v), yet "p proves q v r" is still valid. In this case, we know we can prove q if p is true, and "q v r" can be proven if q is true (using disjunction introduction or addition). (Don't forget that "p v true" is a tautology, meaning it's always true). Therefore, we can prove "q v r" if p is true, no matter what r is.

$\endgroup$
  • $\begingroup$ Welcome to math.SE! This might help you writing better-looking posts. $\endgroup$ – user228113 Jun 22 '15 at 15:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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