Entailment–Unsatisfiability Duality

logic proof-theory

Definition

Entailment–Unsatisfiability Duality

The entailment–unsatisfiability duality is the equivalence between semantic entailment and the unsatisfiability of a counterexample set.

For a set of formulas $\Gamma$ and a formula $Q$,

$$\Gamma \models Q\text{if and only if}\Gamma \cup \{\neg Q\}\text{ is unsatisfiable}.$$

Thus, $\Gamma$ entails $Q$ exactly when there is no interpretation that satisfies all formulas in $\Gamma$ while falsifying $Q$.

Reason

Countermodels

A countermodel to $\Gamma \models Q$ is an interpretation that satisfies every formula in $\Gamma$ but makes $Q$ false.

Making $Q$ false is the same as making $\neg Q$ true. Hence a countermodel exists exactly when

$$\Gamma \cup \{\neg Q\}$$

is satisfiable. Therefore, no countermodel exists exactly when $\Gamma \cup \{\neg Q\}$ is unsatisfiable.

Refutation

The duality justifies proof by refutation.

To prove $\Gamma \models Q$, assume all formulas in $\Gamma$ and also assume $\neg Q$. If these assumptions derive a contradiction, or derive the empty clause $\square$ after conversion to clauses, then $\Gamma \cup \{\neg Q\}$ is unsatisfiable. Hence $\Gamma \models Q$.