# Dupla negação

Na lógica proposicional, a dupla negação é o teorema que afirma que "Se uma declaração é verdadeira, então não é o caso que a declaração não é verdadeira". Isto é expresso ao dizer que uma proposição A é logicamente equivalente a não (não-A), ou pela fórmula A ≡ ~(~A) onde o sinal ≡ exprime a equivalência lógica e o sinal ~ expressa negação.
Como a lei do terceiro excluído, este princípio é considerado uma lei do pensamento na lógica clássica, mas ele não é permitido pela lógica intuicionista. O princípio foi estabelecido como um teorema da lógica proposicional por Russell e Whitehead em Principia Mathematica como:
       $*4\centerdot 13.\vdash .p\equiv \sim (\sim p)$
       "Este é o princípio da dupla negação, isto é, uma proposição é equivalente a falsidade de sua negação."
O principium contradictiones dos lógicos modernos (particularmente Leibniz e Kant) na fórmula A é não não-A, difere inteiramente em significado e aplicação da proposição Aristotélica [ i.e. Lei de Contradição: não (A e não-A) i.e. ~(A & ~A), ou não (( B é A) e (B é não-A))]. Este último refere-se à relação entre um julgamento afirmativo e outro negativo.
De acordo com Aristóteles, um juízo [B é julgado ser um A] contradiz outro [B é considerado ser um não-A]. A proposição posterior [ A não é não-A ] refere-se à relação entre sujeito e predicado em uma única sentença; o predicado contradiz o sujeito. Aristóteles afirma que o juízo é falso quando outro é verdadeiro; escritores posteriores [Leibniz e Kant] determinam que a sentença é em si e absolutamente falsa, porque o predicado contradiz o sujeito. O que os escritores posteriores desejam, é um princípio a partir do qual ele pode saber se certas proposições são verdadeiras nelas mesmas. A partir da proposição Aristotélica não podemos imediatamente inferir a veracidade ou a falsidade de qualquer proposição, mas apenas a impossibilidade de crer afirmação e negação ao mesmo tempo.

## Eliminação da negativa dupla

Eliminação da negativa dupla (também chamada de eliminação da dupla negação, introdução da negativa dupla, introdução da dupla negação, negação dupla, ou eliminação da negação) são duas regras de substituição válidas. Eles são as inferências de que se A é verdadeira, então não não-A é verdadeira e o seu inverso, se não não-A é verdadeira, então A é verdadeira. A regra permite introduzir ou eliminar uma negação de uma prova lógica. A regra é baseada na equivalência de, por exemplo, é falso que não está chovendo. e está chovendo.
A regra da introdução da dupla negação é:
    $$ $P\Rightarrow {\mbox{¬}}{\mbox{¬}}P$
e a regra de eliminação de dupla negação é:
    ${\mbox{¬}}{\mbox{¬}}P\Rightarrow P$
Onde "$\Rightarrow$" é um símbolo da metalógica que representa "pode ser substituído em uma prova por."

### Notação Formal

A regra de introdução da dupla negação pode ser escrito em notação de sequente:
    $$$P\vdash {\mbox{¬}}{\mbox{¬}}P$
A regra de eliminação de dupla negação pode ser escrita como:
    $$${\mbox{¬}}{\mbox{¬}}P\vdash P$
Em regra de inferência:
    $$${P \over {\mbox{¬}}{\mbox{¬}}P}$
e
    $$${{\mbox{¬}}{\mbox{¬}}P \over P}$
ou como uma tautologia (sentença simples de cálculo proposicional):
    $$$P\rightarrow {\mbox{¬}}{\mbox{¬}}P$
e
    $$${\mbox{¬}}{\mbox{¬}}P\rightarrow P$
Estes podem ser combinadas em uma única fórmula bicondicional:
    $$${\mbox{¬}}{\mbox{¬}}P\leftrightarrow P$.
Já que bicondicionalidade é uma relação de equivalência, qualquer instância de ¬¬A em uma fórmula bem-formada pode ser substituída por A, deixando inalterada o valor-verdade da fórmula bem-formada.
Eliminação da negativa dupla é um teorema da lógica clássica, mas não das lógicas mais fracas, tais como a lógica intuicionista e a lógica minimal. Devido ao seu carácter construtivo, uma instrução como Não é o caso de não estar chovendo , é mais fraca do que está chovendo. Este último exige uma prova de chuva, enquanto o primeiro apenas exige uma prova de que a chuva não seria contraditória. (Essa distinção também ocorre em linguagem natural, na forma de lítotes.) A introdução da dupla negação é um teorema das lógicas intuicionista e minimal, como $$.
Na teoria dos conjuntos, temos também a operação de negação do complemento que obedece a esta propriedade: um conjunto A e um conjunto (A$^C$)$^C$ (onde A$^C$ representa o complemento de A) são o mesmo.

## Dupla negação no uso cotidiano

A dupla negação é bem comum na comunicação das pessoas na língua portuguesa e é usada para dar "ênfase na negação". Você poderá encontrar em trechos de músicas, trechos de livros, traduções em geral do inglês. Esse hábito ocorre, em geral, quando são usados termos que representam ausência na frase, tais como nada e nenhum.
| Trecho ou frase | Versão em inglês | Explicação | Uso/Exemplo |
| Há/existe | There is | Tradução literal | Indica presença |
| Não há/existe | There is not | Tradução literal | Indica a não presença |
| Nenhum | none | Tradução literal | Indica Ausencia |
| Há/existe nenhum | There is none | Tradução literal | - Há nenhuma criança no parque. (frase raramente usada). - Não há criança no parque. (frase mais usada, note a falta do termo "nenhum") |
| Não há/existe nenhum | There is none | Dupla negação: "Se uma declaração é verdadeira então não é o caso que a declaração não é verdadeira." | Não há nenhuma criança no parque |
Nem todos os termos que indicam ausência estão inseridos nesse hábito tais como o termo falta:
| Trecho ou frase | Significado | Negação | Significado | Dupla negação |
| Existe nada | Ausência | Não existe nada. | Ausência | SIM |
| Existe Falta | Ausência | Não existe falta. | Contrário de ausência. | NÃO |
| Estou pensando sobre nada. | Nada de pensamentos. | Não estou pensando sobre nada.(frase muito comum) | Nada de pensamentos. | SIM |
| Estou pensando sobre falta de fontes. | O sujeito está pensando sobre ausência de referências. | Não estou pensando sobre falta de fontes. | O sujeito não está pensando sobre ausência de referências. | NÃO |