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 $\mathrm{\neg }\mathrm{\neg }\varphi \equiv \varphi$, die geldt voor alle formules $\varphi$. Anders gezegd geldt dat uit $\mathrm{\neg }\mathrm{\neg }\varphi$ de formule $\varphi$ afleidbaar is: $\mathrm{\neg }\mathrm{\neg }\varphi ⊢\varphi$. Op vergelijkbare wijze kan ook een dubbele negatie geïntroduceerd worden: $\varphi ⊢\mathrm{\neg }\mathrm{\neg }\varphi$.

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

$\frac{\mathrm{\neg }\mathrm{\neg }\varphi }{\varphi }$ $\frac{\varphi }{\mathrm{\neg }\mathrm{\neg }\varphi }$

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 $\varphi ⊢\mathrm{\neg }\mathrm{\neg }\varphi$ geldt ook dat $⊢\varphi \to \mathrm{\neg }\mathrm{\neg }\varphi$ en aangezien $\mathrm{\neg }\mathrm{\neg }\varphi ⊢\varphi$ geldt ook dat $⊢\mathrm{\neg }\mathrm{\neg }\varphi \to \varphi$.

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

Zie ook

• Wet van de uitgesloten derde