# Doppia negazione

Nella logica proposizionale, la doppia negazione è il teorema che afferma che "Se un'affermazione è vera, allora non si dà il caso che l'affermazione non è vera". Ciò si esprime anche dicendo che l'affermazione è logicamente equivalente a non (non A), o tramite la formula A ≡ ~(~A) dove il segno ≡ indica l'equivalenza logica e il segno ~ indica la negazione. In altre parole, due negazioni affermano.
Come la legge del terzo escluso, questo principio è considerato una legge del pensiero della logica classica, ma non è contemplato nella logica intuizionista. Nei Principia Mathematica di Russell e di Whitehead esso fu affermato come un teorema di logica proposizionale:
       $\mathbf {*4\cdot 13} .\ \ \vdash .\ p\ \equiv \ \thicksim (\thicksim p)$
    Questo è il principio della doppia negazione, cioè che "una proposizione è equivalente alla falsità della sua negazione".

## Eliminazione e introduzione

L'eliminazione della doppia negazione o la sua introduzione sono due regole di sostituzione logicamente valide. Sono le inferenze che "se A è vero, allora non non-A è vero" (con la negazione ripetuta due volte), e viceversa che "se non non-A è vero, allora è vero". La regola permette di introdurre o eliminare una negazione da una dimostrazione formale. La regola è basata sull'equivalenza di frasi come "è falso che non stia piovendo" e sta piovendo".
La regola di introduzione della doppia negazione è:
    $P\Rightarrow \neg \neg P$,
mentre al contrario la regola di eliminazione della doppia negazione è:
    $\neg \neg P\Rightarrow P$,
dove "$\Rightarrow$" è un simbolo metalogico che significa "in una dimostrazione può essere sostituito da".
Nella regola di inferenza si ha:
    ${\frac {P}{\neg \neg P}}$
e
    ${\frac {\neg \neg P}{P}}$
o come tautologia:
    $P\to \neg \neg P$
e
    $\neg \neg P\to P$
Queste possono essere combinate in un'unica formula bicondizionale:
    $\neg \neg P\leftrightarrow P$.
Dal momento che un bicondizionale è una relazione di equivalenza, ogni istanza di ¬¬A all'interno di una formula ben formata può essere sostituita da A, lasciando invariato il valore di verità della formula stessa.
L'eliminazione della doppia negazione è un teorema della logica classica, che non appartiene a logiche più deboli come la logica intuizionista e la logica minimale. Invece, l'introduzione della doppia negazione è anche un teorema della logica intuizonista e della logica minimale, essendo vero che $\neg \neg \neg A\vdash \neg A$.
A motivo del loro aspetto costruttivo, proposizioni come "Non si dà il caso che non stia piovendo" sono più deboli della proposizione "Non sta piovendo". La seconda richiede di dimostrare che sta piovendo, mentre la prima richiderebe semplicemente di dimostrare che il fatto che si metta a piovere non è contraddittorio. Questa differenza è recepita nel linguaggio naturale dalla figura retorica della litote.

## Nei sistemi di calcolo proposizionale classico

Nei sistemi deduttivi di Hilbert per la logica proposizionale, la doppia negazione non è sempre considerata un assioma ed è più spesso trattata come un teorema. Descriviamo una dimostrazione di questo teorema nel sistema di tre assiomi proposto da Jan Łukasiewicz:
    A1. $\phi \to \left(\psi \to \phi \right)$
    A2. $\left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)$
    A3. $\left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)$
Usiamo il lemma $p\to p$, che in questa sede è citato come (L1), in aggiunta al seguente lemma:
    (L2) $p\to ((p\to q)\to q)$
Inizialmente si dimostra che $\neg \neg p\to p$. Per brevità, si denota $q\to (r\to q)$ con $\varphi _{0}$. Si utilizzerà ripetutamente il sillogismo ipotetico come scorciatoia per diversi passaggi della dimostrazione.
    (1) $\varphi _{0}$   (istanziazione di (A1))
    (2) $(\neg \neg \varphi _{0}\to \neg \neg p)\to (\neg p\to \neg \varphi _{0})$   (istanziazione di (A3))
    (3) $(\neg p\to \neg \varphi _{0})\to (\varphi _{0}\to p)$   (istanziazione di (A3))
    (4) $(\neg \neg \varphi _{0}\to \neg \neg p)\to (\varphi _{0}\to p)$   (dalla (2) e dalla (3) mediante sillogismo ipotetico come metateorema)
    (5) $\neg \neg p\to (\neg \neg \varphi _{0}\to \neg \neg p)$   (istanziazione di (A1))
    (6) $\neg \neg p\to (\varphi _{0}\to p)$   (dalla (4) e dalla (5) mediante sillogismo ipotetico come metateorema)
    (7) $\varphi _{0}\to ((\varphi _{0}\to p)\to p)$   (istanziazione di (L2))
    (8) $(\varphi _{0}\to p)\to p$   (dalla (1) e dalla (7) mediante modus ponens)
    (9) $\neg \neg p\to p$   (dalla (6) e dalla (8) mediante sillogismo ipotetico come metateorema).
A questo punto, resta da dimostrare che $p\to \neg \neg p$.
    (1) $\neg \neg \neg p\to \neg p$   (istanziazione della prima parte del teorema già dimostrata)
    (2) $(\neg \neg \neg p\to \neg p)\to (p\to \neg \neg p)$   (istanziazione di (A3))
    (3) $p\to \neg \neg p$   (dalla(1) e dalla (2) mediante modus ponens).
E la dimostrazione è così completata.