Dupla negação

Na lógica e na lógica proposicional, as regras de inferência eliminação da dupla negação e introdução da dupla negação permitem eliminar ou introduzir um par de sinais de negação. Essas regras se baseiam na equivalência de, por exemplo,

Não é verdade que não está chovendo

Portanto, está chovendo.

Formalmente, a regra da eliminação da dupla negação é:

$\underline{\lnot \lnot A \quad}\,\!$

$A\,\!$

Formalmente, a regra da introdução da dupla negação é:

$\underline{A \quad \quad}\,\!$

$\lnot \lnot A\,\!$

Essas duas regras — eliminação da dupla negação e introdução da dupla negação — podem ser reformuladas na notação de sequentes:

$\neg \neg A \Longrightarrow A$,

$A \Longrightarrow \neg \neg A$.

Aplicando o Teorema da Dedução em cada uma dessas regras de inferência, é gerado um par de implicações válidas:

$\Longrightarrow \neg \neg A \rightarrow A$,

$\Longrightarrow A \rightarrow \neg \neg A$,

que podem ser combinadas gerando uma única bi-implicação:

$\neg \neg A \leftrightarrow A$.

Como a bicondicional define uma relação de equivalência, qualquer instância de ¬¬A como uma subfórmula de uma fórmula bem formada pode ser substituída por A, sem mudar o valor-verdade da fórmula correspondente.

A eliminação da dupla negação é uma regra válida na lógica clássica, mas não da lógica intuicionista. Uma sentença como Não é verdade que não está chovendo é mais fraca que Está chovendo. Esta última sentença requer uma prova de que está chovendo, enquanto a primeira requer somente uma prova de que a suposição da chuva não seja contraditória. (Essa distinção também ocorre na linguagem natural, na forma de lítotes). Já a introdução da dupla negação é uma regra válida na lógica intuicionista, assim como $\neg \neg \neg A \vdash \neg A$.

Ver também

• Regras de inferência
• Negação