Relationship between satisfiability and entailment (first-order logic)

Entailment and satisfiability are intimately connected.

Theorem Let $\mathcal S$ be a signature, $\mathcal \Phi$ a set of $\mathcal S$-formulas, and $\psi$ an $\mathcal S$-formula.

1. The following are equivalent:
   • $\Phi \models \psi$.
   • $\Phi \cup \{\neg \psi\}$ is unsatisfiable.
2. The following are equivalent:
   • $\Phi$ is satisfiable.
   • $\Phi \not\models \bot$.

Proof The second part follows from the first part. For the proof of the first part, let $\Phi$ be a set of $\mathcal S$-formulas and $\psi$ an $\mathcal S$-formula. We have the following chain of equivalences:

• $\Phi \models \psi$.
• For every $\mathcal S$-structure $\mathcal A$ and every $A$-assignment $\beta$ with $\mathcal A, \beta \mymodels \Phi$, we have $\mathcal A, \beta \mymodels \psi$—definition of $\models$.
• For every $\mathcal S$-structure $\mathcal A$ and every $A$-assignment $\beta$ with $\mathcal A, \beta \mymodels \Phi$, we have $\mathcal A, \beta \not\mymodels \neg \psi$—semantics of $\neg$.
• There is no $\mathcal A$-structure and $A$-assignment $\beta$ such that $\mathcal A,\beta \models \Phi \cup \{\neg\psi\}$—basic reasoning.
• $\Phi \cup \{\neg\psi\}$ is unsatisfiable.

Computational consequence

The most important consequence of the above theorem, from a computational perspective, is that entailment and the complement of satisfiability are interreducible:

Theorem Let $\mathcal S$ be an arbitrary signature. Then entailment (for finite or recursively enumerable sets of formulas) and the complement of satisfiability (for finite sets or recursively enumerable sets of formulas) are interreducible.

Proof For finite sets, the proof is straightforward, given the above theorem.

Here is a reduction from entailment to the complement of satisfiability: $\langle \Phi, \psi\rangle$ is mapped to $\Phi \cup \{\neg\psi\}$.

Here is a reduction from the complement of satisfiability to entailment: $\Phi$ is mapped to $\langle \Phi, \bot\rangle$.

For recursively enumerable sets, the reductions are slightly more complicated. The function $\langle \text{code}(M), \psi\rangle \mapsto \text{code}(M')$, where $M$ is a TM enumerating a set of first-order formulas and $M'$ is a (straightforward) modification of $M$ which enumerates what $M$ enumerates and, in addition, $\neg \psi$, is a reduction from entailment for r.e. sets to the complement of satisfiability for r.e. sets.

Similarly, the function $\text{code}(M) \mapsto \langle \text{code}(M), \bot\rangle$, where $M$ is a TM enumerating a set of first-order formulas, is a reduction from the complement of satisfiability of r.e. sets to entailment for r.e. sets.