La idempotencia de la 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 captada por una regla estructural llamada contracción , y en tales sistemas se puede decir que la implicación es idempotente si y solo si la contracción es una regla admisible .
Regla de contracción: de
se deriva
O en notación de cálculo secuencial ,
En la lógica lineal y afín , la implicación no es idempotente.
