Idempotency of entailment

From Infogalactic: the planetary knowledge core
Jump to: navigation, search

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,

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