Satisfaction (First-Order Logic)

first-order-logic

Definition

Satisfaction (First-Order Logic)

Let $(\mathcal{M},\ell )$ be an interpretation and $\phi$ a formula. The satisfaction relation

$$(\mathcal{M},\ell )\models \phi$$

holds when $\phi$ is true under $\mathcal{M}$ with assignment $\ell$. The definition is inductive.

Notation

The same symbol $\models$ appears in two roles, distinguished by what sits on the left:

Left side	Meaning
$\mathcal{M},\ell \models \phi$	Satisfaction — this particular structure and assignment
$F_1,\dots ,F_n\models G$	Entailment — all structures and assignments

Examples

Consider a structure $\mathcal{M}$ with:

$$\begin{array}{rl}\mathcal{D}& =\{s,d,z\}\\ {\text{socrates}}^{\mathcal{M}}& =s\\ {\text{zeus}}^{\mathcal{M}}& =z\\ {\text{Human}}^{\mathcal{M}}& =\{s\}\\ {\text{Mortal}}^{\mathcal{M}}& =\{s,d\}\end{array}$$

$\text{Human}(\text{socrates})$

${\text{socrates}}^{\mathcal{M}}=s$ and $s\in {\text{Human}}^{\mathcal{M}}$, so

$$\mathcal{M}\models \text{Human}(\text{socrates})$$

$\text{Mortal}(\text{zeus})$

${\text{zeus}}^{\mathcal{M}}=z$ and $z\notin {\text{Mortal}}^{\mathcal{M}}$, so

$$\mathcal{M}/\models \text{Mortal}(\text{zeus})$$

$\exists x\neg \text{Mortal}(x)$

Pick $\ell$ with $\ell (x)=z$. Then

$$\ell (x)\notin {\text{Mortal}}^{\mathcal{M}}$$

so

$$(\mathcal{M},\ell )\models \neg \text{Mortal}(x)$$

Since we found $d=z\in \mathcal{D}$ satisfying the body:

$$(\mathcal{M},\ell )\models \exists x\neg \text{Mortal}(x)$$

$\exists x(\text{Mortal}(x)\wedge \neg \text{Human}(x))$

Pick $\ell$ with $\ell (x)=d$. Then

$$d\in {\text{Mortal}}^{\mathcal{M}}\text{and}d\notin {\text{Human}}^{\mathcal{M}}$$

so

$$(\mathcal{M},\ell )\models \text{Mortal}(x)\wedge \neg \text{Human}(x)$$

Hence

$$(\mathcal{M},\ell )\models \exists x(\text{Mortal}(x)\wedge \neg \text{Human}(x))$$

$\forall x(\text{Human}(x)\to \text{Mortal}(x))$

Let $\ell$ be arbitrary. We check each $e\in \mathcal{D}$:

$\ell [e/x](x)$	$\in {\text{Human}}^{\mathcal{M}}$?	$\in {\text{Mortal}}^{\mathcal{M}}$?	$\text{Human}(x)\to \text{Mortal}(x)$?
$s$	yes	yes	yes — consequent holds
$d$	no	yes	yes — antecedent false
$z$	no	no	yes — antecedent false

All three satisfy the implication, so

$$(\mathcal{M},\ell )\models \forall x(\text{Human}(x)\to \text{Mortal}(x))$$

Since $\ell$ was arbitrary, the sentence is true in $\mathcal{M}$.

Satisfaction vs. Entailment

The examples above check satisfaction in one structure. Entailment is much stronger: it claims something about all possible structures. To show $\text{Human}(\text{socrates})\models \exists x\text{Human}(x)$ you must argue that no structure can make $\text{Human}(\text{socrates})$ true without also making $\exists x\text{Human}(x)$ true — no matter what the domain is or who Socrates names. That is why we need proof systems: you cannot enumerate all structures.