nLab contraction rule

The contraction rule

The contraction rule

Idea

In logic, the contraction rule states that any valid deduction that uses a premise more than once remains valid using that premise only once. Along with the weakening rule and the exchange rule, it is one of the most commonly adopted structural rules.

The contraction rule is not used in all logical frameworks. For instance in linear logic it is discarded.

Statements

Exactly how this looks depends on the logic used.

Semantics

This rule corresponds to having diagonals for the monoidal structure corresponding to the logical binary operator at hand.

References

The notion of contraction as a structural inference rule originates (under the German name Zusammenziehung) with:

On the categorical semantics:

Discussion in dependent type theory:

Last revised on August 25, 2023 at 15:11:42. See the history of this page for a list of all contributions to it.