# Doble negación (lógica)

En lógica proposicional, la doble negación es el teorema que afirma que "Si un enunciado es verdadero, entonces no es el caso que la declaración no es cierta". Esto se expresa diciendo que una proposición A es lógicamente equivalente a no (no-A), o por la fórmula A≡~(~A) donde el signo ≡ expresa equivalencia lógica y el signo ~ expresa negación.
Al igual que la ley del tercero excluido, este principio es considerado como ley del pensamiento en la lógica clásica, aunque la lógica intuicionista no lo permite.

## Historia

El principio fue declarado por Russell y Whitehead como teorema de la lógica proposicional en Principia Mathematica como:
       $\mathbf {*4\cdot 13} .\ \ \vdash .\ p\ \equiv \ \thicksim (\thicksim p)$
       "Este es el principio de la doble negación, es decir, una proposición es equivalente a la falsedad de su negación."
El principium contradictiones de los lógicos modernos (especialmente Leibnitz y Kant) en la fórmula A es no no-A, difiere totalmente de significado y la aplicación desde la proposición aristotélica [es decir, la Ley de Contradicción: no (A y no-A), es decir ~(A y ~A), o no ((B es A) y (B es no-A))]. Esta última se refiere a la relación entre una afirmación y un juicio negativo.
Según Aristóteles, una sentencia [B se juzga como un A] contradiciendo a la otra [B se juzga como un no-A]. La proposición posterior [A no es no-A] se refiere desde la relación entre el sujeto y el predicado en un solo juicio, el predicado contradice el tema. Aristóteles afirmaba que una sentencia es falsa cuando otra es verdadera, escritores posteriores [Leibniz y Kant] afirmaban que un juicio es en sí mismo y absolutamente falso, porque el predicado contradice al tema. Lo que los escritores posteriores desean es un principio desde el cual se puede saber si ciertas proposiciones son verdaderas en sí mismas. De la proposición aristotélica no es posible inferir inmediatamente la verdad o falsedad de una proposición particular, sino solamente la imposibilidad de creer tanto en la afirmación como en la negación, al mismo tiempo.

## Eliminación de la doble negación

La doble negación puede eliminarse mediante la eliminación de la doble negación (también llamada eliminación del negativo doble, introducción del doble negativo, introducción de la doble negación, o simplemente doble negación). Esta se realiza mediante dos reglas de reemplazo válidas. Son las inferencias que si A es verdad, entonces no no-A es verdad y su conversión, que, si no no-A es verdad, entonces A es verdad. La norma permite introducir o eliminar una negación de una prueba lógica. La norma se basa en la equivalencia de, por ejemplo, es falso que no está lloviendo y está lloviendo.
La regla de introducción de la doble negación es:
    P $\Leftrightarrow$ ¬¬P
y la regla eliminación de la doble negación es:
    ¬¬P $\Leftrightarrow$ P
Donde "$\leftrightarrow$" es un símbolo metalógico que representa "puede ser reemplazado en una prueba con... ."

## Notación formal

La regla de introducción de la doble negación puede escribirse en la notación subsiguiente:
    $P\vdash \neg \neg P$
La regla de eliminación de la doble negación se puede escribir como:
    $\neg \neg P\vdash P$
En forma de regla:
    ${\frac {P}{\neg \neg P}}$
y
    ${\frac {\neg \neg P}{P}}$
o como la afirmación de una verdadera tautología (sentencia simple de cálculo proposicional):
    $P\to \neg \neg P$
y
    $\neg \neg P\to P$
Estos se pueden combinar en una sola fórmula bicondicional:
    $\neg \neg P\leftrightarrow P$.
Puesto que la bicondicionalidad es una relación de equivalencia, cualquier instancia de ¬¬A en una fórmula bien formada puede ser sustituida por A, dejando sin cambios el valor de verdad de la fórmula bien formada.

### Usos e implicaciones

La eliminación de la doble negación es un teorema de la lógica clásica, pero no de la lógica más débil, como la lógica intuicionista y la lógica mínima. Debido a su carácter constructivo, una sentencia como No es el caso de que no llueve es más débil que Está lloviendo. Esta última requiere una prueba de lluvia, mientras que la primera se limita a exigir una prueba de que llueve no sería contradictorio. (Esta distinción también se plantea en lenguaje natural en forma de litotes.) La introducción de la doble negación es un teorema tanto de la lógica intuicionista como de la lógica mínima, como es $\neg \neg \neg A\vdash \neg A$.
En la teoría de conjuntos también tenemos la operación de negación del complemento que obedece a esta propiedad: un conjunto A y un conjunto (A$^C$)$^C$ (donde A$^C$ representa el complemento de A) son los mismos.