Idempotency of entailment
From Wikipedia, the free encyclopedia
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. In sequent calculi this property can be captured by a structural rule called contraction and in such systems one may say that entailment is idempotent just in case contraction is an admissible rule.
Formally: (A → (A → B)) → (A → B)