= Solution
The <first-order terms> are the smallest collection containing every variable and $c$ and containing $F(s,t)$ whenever $s,t$ are <first-order terms>. The <atomic formulas> are exactly $s\approx t$ for <first-order terms> $s,t$. <Logical formulas> are then obtained from <atomic formulas> by the <logical connectives> and <quantifiers>: if $\theta,\psi$ are <logical formulas> and $x$ a variable, then $\neg\theta$, $(\theta\wedge\psi)$, $(\theta\vee\psi)$, $(\theta\to\psi)$, $\forall x\theta$ and $\exists x\theta$ are <logical formulas>. These closure rules, with no additional strings admitted, define the syntax; a presentation using fewer primitive connectives treats the others as abbreviations.
<Semantic entailment> is the condition
$$
\boxed{\Gamma\models\phi\quad\Longleftrightarrow\quad
\text{for every }\mathfrak A\text{ and every assignment }v,
\bigl(\mathfrak A\models\gamma[v]\text{ for all }\gamma\in\Gamma\bigr)
\Longrightarrow\mathfrak A\models\phi[v].}
$$
The same <first-order variable assignment> is used for all premises and the conclusion. This matters when <free variables> occur; for <first-order sentences> the <truth value> is independent of the <first-order variable assignment>.
Back to article page
