[Math] Weakening and Contraction

Question

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?

Answer 1

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.