Definition
Entailment–Unsatisfiability Duality (Propositional Logic)
The entailment–unsatisfiability duality is the equivalence between semantic entailment and the unsatisfiability of a counterexample set.
For a set
of propositional formulas and a propositional formula , Thus,
entails exactly when there is no interpretation that satisfies all formulas in while falsifying .
Reason
Countermodels
A countermodel to
is an interpretation that satisfies every formula in but makes false. Making
false is the same as making true. Hence a countermodel exists exactly when is satisfiable. Therefore, no countermodel exists exactly when
is unsatisfiable.
Refutation
The duality justifies proof by refutation.
To prove