Idempotency of entailment

Idempotency of entailment is a property of logical systems that states that one may derive the same consequences from many instances of a hypothesis as from just one. This property can be captured by a structural rule called contraction , and in such systems one may say that entailment is idempotent if and only if contraction is an admissible rule.

Rule of contraction: from

A,C,C → B

is derived

A,C → B.

Or in sequent calculus notation,

${\displaystyle {\frac {\Gamma ,C,C\vdash B}{\Gamma ,C\vdash B}}}${\displaystyle {\frac {\Gamma ,C,C\vdash B}{\Gamma ,C\vdash B}}}

In linear and affine logic, entailment is not idempotent.

• No-deleting theorem

• Logical consequence
• Theorems in propositional logic
• Logic stubs

• Articles lacking sources from December 2009
• All articles lacking sources
• All stub articles