1
$\begingroup$

Wikipedia says that 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$
  • $\begingroup$ The article you link talks about concepts of formal logic. Your tags indicate that you try to understand them as programming language constructs. Could this be the source of your confusion? $\endgroup$ – FrankW Sep 16 '14 at 6:44
  • $\begingroup$ @FrankW yes. I'm currently a little lost with these concepts in relation to programming languages. $\endgroup$ – Tamad Lang Sep 16 '14 at 8:43
3
$\begingroup$

I can't comment about the programming language aspect, but here is the logical aspect. A sequent is an expression of the form $$ A_1,\ldots,A_n \vdash B_1,\ldots,B_m $$ whose meaning is "if $A_1,\ldots,A_n$ hold then one of $B_1,\ldots,B_m$ holds", that is $$ (A_1 \land \cdots \land A_n) \to (B_1 \lor \cdots \lor B_m). $$ Sequent calculus is nice since its laws enjoy a certain symmetry between the two sides that reflects the de Morgan symmetry between AND and OR.

Weakening is the law that states that you can a formula to either side of a sequent. That is, if a sequent $\Gamma \vdash \Delta$ is true (where $\Gamma,\Delta$ are sequences of propositions), then for every formula $X$, both sequents $\Gamma,X \vdash \Delta$ and $\Gamma \vdash \Delta,X$ also hold.

Contraction states that if a formula appears twice one of the sides, then an equivalent sequent is obtained by removing the duplicate. That is, if $\Gamma,X,X \vdash \Delta$ then also $\Gamma,X \vdash \Delta$, and similarly for duplicates on the other side.

One more structural rule, permutation, allows us to reorder formulas: if $\Gamma,X,Y,\Delta \vdash E$ then also $\Gamma,Y,X,\Delta \vdash E$, and the same for the other side.

$\endgroup$

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.