Introduction to Logic

Unsatisfiability Theorem

The Unsatisfiability Theorem states that Δ ⊨ φ if and only if Δ ∪ {¬φ} is unsatisfiable. In other words, if a set Δ of sentences logically entails a sentence φ, then Δ together with the negation of φ must be unsatisfiable, and vice versa. The theorem is useful because it assure us that, if we want to determine whether or not Δ ⊨ φ, all we need to do is to determine whether or not Δ ∪ {¬φ} is unsatisfiable, which is often an easier task.