HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

Why contraction and weakening rules are the upside down?

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
whytheareweakeningcontractiondownandrulesupside

Problem

On the A taste of linear logic paper, the author claims that:


A rule consists of zero or more judgements written above a line, and one
judgement written below. If all the judgements above the line are derivable, then the judgement below is derivable also.

He then proceeds to show the following rules:

He then describes those rules as:


Contraction expresses that any hypothesis may be duplicated, and Weakening expresses that any hypothesis may be discarded.

That looks upside down. Reading the "Contraction" rule in English, we have that "if assumptions Γ, A, A imply B, then assumptions Γ, A also imply B" - notice that we discarded an assumption instead of duplicating it. Similarly, the "Weakening" rule adds an assumption to the conclusion, rather than discarding one from the premises as the author seems to suggest. Why?

Solution

Contraction is called contraction because it contracts the two hypotheses into one: $A, A$ is contracted into $A$. Weakening is called weakening because it allows one to deduce a weaker fact: $\Gamma \vdash B$ is stronger than $\Gamma, A \vdash B$ since fewer hypotheses are needed to obtain the conclusion. The names come from forward reasoning: deducing facts from other facts. When you're deducing new truths, you can take already-proven truths and add hypotheses or remove duplicated hypotheses.

When you look at contraction from the point of few of backward reasoning, i.e. examining why a fact might be true, then the contraction duplicates a hypothesis. Similarly the weakening rule discards a hypothesis. When you're trying to prove a goal, you can duplicate or discard hypotheses to get a new goal whose truth implies the truth of the original goal.

Context

StackExchange Computer Science Q#64620, answer score: 7

Revisions (0)

No revisions yet.