Law of excluded middle: is ⊨ p∨¬p valid?

p ∨ ¬p is true in every row and needs no premises at all: every proposition is either true or false, with no third option.

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. 1False: p∨¬pnegated conclusion
    1. 2False: pfrom line 1
      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