How can we introduce double-negation? For example, p is the same as ~~p.

I am not able to find how to introduce ~~ in https://proofs.openlogicproject.org/

Is there anything like DNI, similar to DNE?

  • If i said 'This is not not a hat..', it wouldn't be the same as asserting the things straightforward hatness..
    – CriglCragl
    May 28, 2023 at 19:33
  • That site might not have a way to derive DNI. The Wikipedia article on double negation gives a system with a derivation of DNI, but I'm not competent to translate that system into the one the linked-to site is using. May 28, 2023 at 21:15

1 Answer 1


Suppose ¬p. This contradicts p (by rule ¬E). Therefore, ¬¬p (by rule ¬I).

  • I followed this idea. I was curious whether there is a DNI
    – DEE_GEE
    May 28, 2023 at 21:47

Not the answer you're looking for? Browse other questions tagged .