A structure (or model) $\mathcal{M}$ for a first-order language $\mathcal{L}$ consists of:

1. A non-empty set $M$ called the domain (or universe)
2. For each constant symbol $c$ in $\mathcal{L}$, an element $c^\mathcal{M} \in M$
3. For each $n$-ary function symbol $f$ in $\mathcal{L}$, a function $f^\mathcal{M}: M^n \to M$
4. For each $n$-ary predicate symbol $P$ in $\mathcal{L}$, a relation $P^\mathcal{M} \subseteq M^n$

Given a structure $\mathcal{M}$ and a variable assignment $s: \text{Var} \to M$, we define when $\mathcal{M}$ satisfies a formula $\phi$ under $s$, written $\mathcal{M} \models \phi[s]$:

• $\mathcal{M} \models P(t_1, \ldots, t_n)[s]$ iff $(t_1^\mathcal{M}[s], \ldots, t_n^\mathcal{M}[s]) \in P^\mathcal{M}$
• $\mathcal{M} \models \neg \phi[s]$ iff $\mathcal{M} \not\models \phi[s]$
• $\mathcal{M} \models \phi \land \psi[s]$ iff $\mathcal{M} \models \phi[s]$ and $\mathcal{M} \models \psi[s]$
• $\mathcal{M} \models \forall x \, \phi[s]$ iff $\mathcal{M} \models \phi[s']$ for all $s'$ that differ from $s$ at most on $x$
• $\mathcal{M} \models \exists x \, \phi[s]$ iff $\mathcal{M} \models \phi[s']$ for some $s'$ that differs from $s$ at most on $x$

For sentences (closed formulas), satisfaction is independent of the assignment $s$.

A formula $\phi$ is:

• Valid (or logically true), written $\models \phi$, if $\mathcal{M} \models \phi[s]$ for all structures $\mathcal{M}$ and assignments $s$
• Satisfiable if $\mathcal{M} \models \phi[s]$ for some structure $\mathcal{M}$ and assignment $s$
• Unsatisfiable if it is not satisfiable