Satisfiability and entailment in propositional logic

There is an intimate connection between satisfiability and entailment (in propositional logic).

Theorem Let $\Phi$ be a set of propositional formulas and $\psi$ a propositional formula. Then \begin{align} \Phi \models \psi \qquad \text{iff} \qquad \text{Unsat } \Phi \cup \{\neg \psi\}\enspace. \end{align} Similarly, \begin{align} \text{Unsat } \Phi \qquad \text{iff} \qquad \Phi \models \bot \enspace. \end{align}

For the proof of the first part, let $\Phi$ be a set of propositional formulas and $\psi$ a propositional formula. For the direction from left to right, assume $\Phi \models \psi$ and, for contradiction, that $\Phi \cup \{\neg \psi\}$ is satisfiable. Then there is a variable assignment such that $\beta \mymodels \varphi$ for every $\varphi \in \Phi$ and $\beta \mymodels \neg \psi$. By the semantics of propositional logic, $\beta \not\mymodels \psi$ follows. Therefore, $\psi$ is not a consequence of $\Phi$---a contradiction.

For the direction from right to left, assume $\Phi \cup \{\neg \psi\}$ is not satisfiable and that $\beta$ is any variable assignment such that $\beta \mymodels \Phi$. To be shown: $\beta \mymodels \psi$. For contradiction, assume $\beta \not\mymodels \psi$. Then $\beta \mymodels \neg \psi$, which implies $\beta \mymodels \Phi \cup \{\neg \psi\}$. So $\Phi \cup \{\neg \psi\}$ is satisfiable---a contradiction.

The second part is an immediate consequence of the first part.

As a consequence of this theorem, satisfiability tests can be used for checking entailment.