Contraction Glossary
Definition
Contraction is the logical principle that whatever follows from two assumptions of the same formula also follows from just one assumption of that formula. This emerges in the natural deduction calculus in the form of discharge rules which allow an assumption to be discharged without residue even if it has been used more than once to obtain the proof.
Comments
This is a subtle feature of classical logic and similar logics (including relevant and constructive logics) which is so natural that it could go unnoticed except that it produces some of the distinctive features of these systems. In proofs, we usually apply it implicitly, without even noticing that it is there.
Contraction is inevitable if we think of the premises of an argument, or of a sequent as coming simply in a set, because the set {a,a} is the same as {a}. However, the fuzzy logic described towards the end of these notes shows one way of formulating logic without it.
Examples
-
Extracting the two conjuncts of assumption 1 does not require contraction, but lines 2 and 3 are essentially applied to each other to produce line 4, which counts as using assumption 1 twice. There is some non-trivial logic packed into the idea that lines 4 and 5 say the same thing. -