Double negation: is ¬¬p ⊨ p valid?

¬¬p and p are true in the same rows, so a doubled negation can be dropped wherever it stands. Two negations cancel.

Valid¬¬p ⊨ p

Every branch of the tableau closes, so nothing makes the premises true and the conclusion false at once.

Proof (semantic tableau)

  1. 1True: ¬¬ppremise
    1. 2False: pnegated conclusion
      1. 3False: ¬pfrom line 1
        1. 4True: pfrom line 3

          Branch closed: line 4 contradicts line 2.

closed branch

How semantic tableaux work →

Try in Calculator

More worked proofs