Entailment (First-Order Logic)

first-order-logic

Definition

Entailment (First-Order Logic)

Let $F_1,\dots ,F_n,G$ be formulas. Then $F_1,\dots ,F_n$ entail $G$, written

$$F_1,\dots ,F_n\models G$$

if for every structure $\mathcal{M}$ and every variable assignment $\sigma$:

$$\mathcal{M},\sigma \models F_i\text{ for all }i⟹\mathcal{M},\sigma \models G$$

Intuition

Entailment is a claim about all possible worlds. You are saying: no matter how I interpret the symbols — no matter what domain I pick, what the constants name, what the predicates mean — whenever I make the premises true, the conclusion is forced to be true.

What "for every structure" means

A structure fixes what the symbols stand for: which set $\mathcal{D}$ the variables range over, which object each constant names, which function each function symbol denotes. The definition says: no matter how you interpret the symbols, if the premises come out true, the conclusion is forced.

This is what makes entailment semantic rather than syntactic. You are not checking a proof — you are checking all possible meanings.

Entailment vs. implication

Entailment ($\models$) lives outside the logic: it is a statement about formulas. Implication ($\to$) lives inside the logic: it is a connective that builds a new formula.

$$F\to G\text{ is a formula.}F\models G\text{ is a claim about formulas.}$$

All humans are mortal

Let $F_1=\forall x(\text{Human}(x)\to \text{Mortal}(x))$ and $F_2=\text{Human}(\text{Socrates})$. Then

$$F_1,F_2\models \text{Mortal}(\text{Socrates})$$

No structure can make Socrates human and all humans mortal without making Socrates mortal. The conclusion is forced.

Two structures, one entailment

Claim: $P(a)\models \exists xP(x)$.

Structure	$\mathcal{D}$	$a^{\mathcal{M}}$	$P^{\mathcal{M}}$	Premise $P(a)$ true?	Conclusion $\exists xP(x)$ true?
${\mathcal{M}}_1$	$\{1,2,3\}$	$1$	$\{1\}$	yes	yes
${\mathcal{M}}_2$	$\{\text{apple},\text{banana}\}$	apple	$\varnothing$	no	—

${\mathcal{M}}_1$ makes the premise true and the conclusion holds. ${\mathcal{M}}_2$ makes the premise false, so it is irrelevant.

No structure makes the premise true and the conclusion false — that is what $\models$ means.

Entailment vs. Satisfaction

The symbol $\models$ is overloaded:

Left side	Meaning	Quantifier
$\mathcal{M},\ell \models \phi$	Satisfaction — $\phi$ is true under this structure and assignment	for one $(\mathcal{M},\ell )$
$F_1,\dots ,F_n\models G$	Entailment — $G$ must be true whenever the premises are	for all $(\mathcal{M},\ell )$

Satisfaction checks one interpretation. Entailment checks them all.

Reductions

These equivalences connect the semantic notions:

$$\begin{array}{rl}\models \phi & ⟺\neg \phi \text{ is unsatisfiable}\\ \phi \text{ is satisfiable}& ⟺/\models \neg \phi \\ \Gamma \models \phi & ⟺\Gamma \cup \{\neg \phi \}\text{ is unsatisfiable}\end{array}$$

Here “unsatisfiable” means unsatisfiable formula and “satisfiable” means satisfiable formula.

For finite $\Gamma$:

$$\Gamma \models \phi ⟺\models \left(\underset{\gamma \in \Gamma }{\bigwedge }\gamma \right)\to \phi$$