Evaluating First-Order Formulas in a Structure

A first-order structure (interpretation) $\mathcal{M}$ fixes the meaning of an otherwise abstract formula. It supplies

• a non-empty domain $D$ (the universe the variables range over),
• a concrete relation $A^{\mathcal M} \subseteq D^k$ for every $k$-ary predicate symbol $A$,
• a concrete function $f^{\mathcal M} : D^m \to D$ for every $m$-ary function symbol $f$,
• and a variable assignment $s$ giving each free variable $x_i$ a value $s(x_i) \in D$.

Deciding whether $\mathcal{M}$ with assignment $s$ satisfies a formula $\varphi$ — written $\mathcal{M} \models \varphi[s]$ — means evaluating $\varphi$ after substituting all these meanings.

Evaluating from the inside out

1. Terms. Replace each variable by its assigned value and each function symbol by its interpretation, then compute. E.g. with $f^{\mathcal M}(x)=2x$, the term $f(x_2)$ evaluates to $2\,s(x_2)$.
2. Atomic formulas. $A(t_1,\dots,t_k)$ is true iff the tuple of evaluated terms lies in the relation: $(\,[\![t_1]\!],\dots,[\![t_k]\!]\,) \in A^{\mathcal M}$. If $A$ is interpreted as $<$, then $A(t_1,t_2)$ just means $[\![t_1]\!] < [\![t_2]\!]$.
3. Connectives. Combine truth values with the usual rules for $\neg,\ \wedge,\ \vee,\ \rightarrow$.
4. Quantifiers. $\forall x_i\,\psi$ is true iff $\psi$ holds for every value of $x_i$ in $D$; $\exists x_i\,\psi$ is true iff $\psi$ holds for at least one value. A sentence (no free variables) is then either true or false in $\mathcal{M}$ independently of $s$.

The recipe

Substitute the interpretations to turn the symbolic formula into an ordinary mathematical statement about the domain $D$, then check that statement.

For quantifier-free formulas with free variables, the assignment $s$ supplies the values $s(x_i)$ and you simply compute. For quantified sentences, reason about whether a suitable witness exists (for $\exists$) or whether the property survives a worst-case choice (for $\forall$); the order of nested quantifiers matters.

Mini-example

Let $D=\mathbb{N}$, interpret $A$ as $<$ and $f$ as $f(x)=2x$, and consider $A(f(x_2), x_4)$. Substituting gives the statement

$2\,s(x_2) < s(x_4).$

If the assignment comes from the sequence $s=\langle 2,4,6,8,\dots\rangle$ (so $s(x_i)=2i$), then $s(x_2)=4$ and $s(x_4)=8$, and we test $2\cdot 4 < 8$, i.e. $8<8$ — false, so $s$ does not satisfy the formula. For $s'=\langle 3,6,9,12,\dots\rangle$ (so $s'(x_i)=3i$) we test $2\cdot 6 < 12$, i.e. $12<12$ — also false. Both fail because doubling the 2nd term lands exactly on the 4th.

Now a quantified sentence on $D=\mathbb{Z}$ with $A$ as $\le$ and $f(x)=x-1$:

$\alpha = \exists x_2\,\forall x_1\; A(f(x_1),x_2) \;\equiv\; \exists x_2\,\forall x_1\,(x_1-1 \le x_2).$

This claims $\mathbb{Z}$ has an upper bound — false, since for any $x_2$ pick $x_1=x_2+2$ to break it. By contrast $\beta=\exists x_3\,A(f(x_3),x_3)\equiv\exists x_3\,(x_3-1\le x_3)$ holds for every $x_3$, so it is true.

Pitfall: an atom is only as good as the relation behind the symbol. With $A$ meaning strict $<$, equality $a=a$ makes $A(a,a)$ false; with $A$ meaning $\le$ it is true. Always re-read whether the interpreted relation is strict or non-strict (and respect quantifier order — $\exists\forall$ and $\forall\exists$ are not interchangeable) before declaring a formula satisfied.