# Relationship between satisfiability and entailment (first-order logic)

### From Learning Logic for Computer Science

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.

- The following are equivalent:
- $\Phi \models \psi$.
- $\Phi \cup \{\neg \psi\}$ is unsatisfiable.

- 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.