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 In proof theory, a structural rule is an inference rule that does not refer to any logical connective, but instead operates on the judgment or sequents directly. Structural rules often mimic intended meta-theoretic properties of the logic. Logics ...

called

contraction Contraction may refer to: Linguistics * Contraction (grammar), a shortened word * Poetic contraction, omission of letters for poetic reasons * Elision, omission of sounds ** Syncope (phonology), omission of sounds in a word * Synalepha, merged ...

, and in such systems one may say that entailment is idempotent if and only if contraction is an

admissible rule In logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is ...

. Rule of contraction: from :''A'',''C'',''C'' → ''B'' is derived :''A'',''C'' → ''B''. Or in sequent calculus notation, :

\frac

In linear and affine logic, entailment is not idempotent.

See also