1. In proof theory, a structural rule according to which one may elide a redundant instance of a formula $\phi$ from a cedent $\Gamma$ whenever two or more instances of $\phi$ appear in $\Gamma$. More formally, this is represented in left and right versions:

2. When $\to$ is a conditional connective, the classically valid inference

Contraction in this form plays an especially important role in the formulation of Curry’s paradox, which has motivated support for contraction-free logics. The axiomatic representation of the foregoing inference frequently appears as:

• • $\left(\phi \to \left(\phi \to \psi \right)\right)\to \left(\phi \to \psi \right)$

3. In belief revision, an operation that removes a sentence from a belief set.