Eliminatie van dubbele negatie

In de klassieke logica is eliminatie van dubbele negatie (ook: dubbele negatie-eliminatie) een afleidingsregel die stelt dat twee opeenvolgende negaties weggehaald mogen worden aangezien de resulterende formule logisch equivalent is met de voorgaande. Deze afleidingsregel maakt gebruik van de gelijkheid $\neg \neg \phi \equiv \phi$, die geldt voor alle formules $\phi\!$. Anders gezegd geldt dat uit $\neg \neg \phi$ de formule $\phi\!$ afleidbaar is: $\neg \neg \phi \vdash \phi$. Op vergelijkbare wijze kan ook een dubbele negatie geïntroduceerd worden: $\phi \vdash \neg \neg \phi$.

De afleidingsregels van het elimineren en introduceren van de dubbele negatie worden respectievelijk ook genoteerd als:

$\frac{\neg \neg \phi}{\phi}$ $\frac{\phi}{\neg \neg \phi}$

Intuïtief zeggen deze regels dat de volgende twee stellingen aan elkaar gelijk zijn:

Het is niet zo dat het niet regent.

Het regent.

Aangezien $\phi \vdash \neg \neg \phi$ geldt ook dat $\vdash \phi \rightarrow \neg \neg \phi$ en aangezien $\neg \neg \phi \vdash \phi$ geldt ook dat $\vdash \neg \neg \phi \rightarrow \phi$.

Dit betekent ook dat de volgende bi-implicatie geldt: $\vdash \neg \neg \phi \leftrightarrow \phi$. Aangezien een bi-implicatie een equivalentierelatie is, kan elk voorkomen van $\neg \neg \phi$ vervangen worden door $\phi\!$ zonder de waarheidswaarde van een formule te veranderen.

Zie ook

• Wet van de uitgesloten derde