La regla en lógica clásica (proposicional y de primer orden) según la cual una fórmula A es lógicamente equivalente a su doble negación ¬¬A, permitiendo inferencia en ambos sentidos entre A y ¬¬A.

Principio

En la lógica clásica la negación es involutiva: aplicar la negación dos veces devuelve la proposición original, de modo que A ↔ ¬¬A es válida y puede emplearse para introducir o eliminar pares de negaciones.

Demostración

Si el enunciado «Está lloviendo» es verdadero, entonces el enunciado «No es cierto que no está lloviendo» también lo es; a la inversa, en lógica clásica la verdad de «No es cierto que no está lloviendo» implica «Está lloviendo».

Aplicación incorrecta

Suponer ¬¬A → A en contextos constructivos o intuicionistas donde esa implicación no se demuestra; usar la eliminación de la doble negación para reclamar una existencia constructiva a partir de ¬¬∃x P(x) sin proporcionar testigo.

Consecuencia

Permite simplificar fórmulas suprimiendo negaciones redundantes en pruebas clásicas y posibilita formas normales y equivalencias que dependen de la eliminación de la negación.

Inversión

Por contraste, la no equivalencia en lógicas constructivas muestra que, si bien A → ¬¬A suele ser demostrable, la recíproca ¬¬A → A falla sin principios clásicos como el principio del tercero excluido.

Límite

Se cumple en la lógica proposicional y de primer orden clásicas; no se aplica en general en lógicas intuicionistas, mínimas o en algunas lógicas paraconsistentes donde la eliminación de la doble negación es inválida o restringida.

Tensión semántica

Tensión entre la identificación clásica de la verdad con la doble negación y los significados constructivos de existencia y prueba, donde ¬¬A es más débil que A porque carece de un testigo constructivo directo.

Síntesis

El Principio De Doble Negación encapsula la intuición clásica de que negar una negación recupera la afirmación original: en sistemas clásicos A y ¬¬A son intercambiables, mientras que en marcos constructivos subraya la diferencia entre demostrabilidad y mera no-refutabilidad.