Propositielogica: Natuurlijke deductie
Dubbele negatie-eliminatieregel
Met de redeneerregels die we tot nu toe behandeld hebben zijn we aanbeland bij een bewijssysteem van intuïtionistische logica, waarin de regel van de uitgesloten derde \(p \lor \neg\, p\) niet als stelling gehanteerd wordt. In de klassieke propositielogica willen we deze regel wel hebben en daarvoor introduceren we de dubbele negatie-eliminatieregel.
Eliminatieregel voor dubbele negatie De eliminatieregel \(\neg\neg\,\mathrm{E}\) voor de dubbele negatie: \[\begin{array}{l|ll} \vdots & \vdots &\\ k &\neg\neg\,\varphi & \\ \vdots & \vdots & \\ l & \varphi& \neg\neg\,\mathrm{E}, k \end{array}\]
Dubbele negatie vs bewijs uit het ongerijmde Het bewijs uit het ongerijmde kom je in de volgende vorm van een redeneerregel ook tegen in de literatuur:
Met de dubbele negatie-regel kunnen we deze redeneerregel ook afleiden m.b.v. de eerdere redeneerregels:
Omgekeerd kan je de dubbele negatie-redeneerregel afleiden uit bovenstaande regel voor het bewijs uit het ongeeijmde:
Kortom, het maakt voor de klassieke propositielogica niet uit of je de dubbele negatie-redeneerregel gebruikt of de regel die het bewjs uit het ongerijmde binnen een afleiding toestaat.
Met de dubbele negatie-regel kunnen we de formule \(p\lor \neg\,p\) wel zonder premissen bewijzen:
