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

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

  • The rule is DNE and it is listed on the right of the screen: Derived Rules. May 23, 2023 at 6:00
  • 1
    Is that all you're having trouble with? Kristian Berry saves the day with her answer, complete with illustrations, pro bono. In the 22nd century?! Am I dreaming mon ami? May 23, 2023 at 6:27
  • Fantastic. I was trying to put ~~E. Now, it is clear.
    – DEE_GEE
    May 23, 2023 at 14:03
  • Is there a double-not introduction rule? Something like DNI? For example, p is equivalent to ~~p, without going throug p, ~p, contradiction, and then not not p
    – DEE_GEE
    May 24, 2023 at 19:23

1 Answer 1


Note that they have DNE in their sidebar:

enter image description here

So, click CREATE PROBLEM, put ~~A on line 1 and A for the conclusion. Then click NEW LINE, put A in the first box, then put "DNE, 1" in the box to the right. Click CHECK PROOF.

enter image description here

Now, this may provide the answer to your question, and the Philosophy SE might be about analyzing arguments logically and all, but your issue seems to be a software consideration, not a philosophical one, so please don't accept my answer even if it's sufficient, I don't think I've earned the points for that. (Moreover, then, the OP question is liable to be closed/deleted anyway, so it wouldn't do me any good to get the points, aye?)

You must log in to answer this question.

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