Set of Literals Satisfiable iff No Complementary Pairs
Theorem
Then $S$ is satisfiable if and only if it contains no complementary pairs.
Proof
Necessary Condition
Suppose $S$ contained the complementary pair $\set {p, \neg p}$.
By the Principle of Non-Contradiction, $\set {p, \neg p}$ is unsatisfiable.
By Superset of Unsatisfiable Set is Unsatisfiable, so is $S$.
Hence if $S$ is satisfiable, it cannot contain any complementary pairs.
$\Box$
Sufficient Condition
Suppose $S$ contains no complementary pair.
Define the boolean interpretation $v: \PP_0 \to \set {\T, \F}$ by:
- $\map v p = \begin{cases} \T & \text{if } p \in S \\ \F & \text{otherwise} \end{cases}$
Let $\mathbf A \in S$ be an arbitary literal.
If $\mathbf A = p$ is a positive literal, then $\map v {\mathbf A} = \T$ is true by the first clause of the definition.
Now suppose $\mathbf A = \neg p$ is a negative literal.
Then $p \notin S$, for $S$ contains no complementary pairs.
Therefore $\map v p = \F$, and hence:
- $\map v {\neg p} = \map v {\mathbf A} = \T$
Since $v$ has been demonstrated to be a model of $S$, $S$ is satisfiable.
$\blacksquare$
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.6.1$: Theorem $2.60$