Modus tollens: is p→q, ¬q ⊨ ¬p valid?

If p → q holds and q is false, p must be false too: anything that made p true would make q true. Denying the consequent denies the antecedent.

Validp→q, ¬q ⊨ ¬p

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

Proof (semantic tableau)

  1. 1p→qpremise
    1. 2¬qpremise
      1. 3¬pnegated conclusion
        1. 4q
          1. 5p
            1. 6p

            2. 7q

closed branch

How semantic tableaux work →

Try in Calculator

More worked proofs