La idempotencia de implicación es una propiedad de los sistemas lógicos que establece que se pueden derivar las mismas consecuencias de muchas instancias de una hipótesis que de una sola. Esta propiedad puede ser capturada por una regla estructural llamada contracción , y en tales sistemas se puede decir que la vinculación es idempotente si y solo si la contracción es una regla admisible .
Regla de contracción: de
- A , C , C → B
es derivado
- A , C → B .
O en notación de cálculo secuencial ,