Solution (source code)

= Solution

A <prime model> of a <complete theory> $T$ is a <first-order model> admitting an elementary <embedding of first-order structures> into every <first-order model> of $T$. Let $\mathcal A\models T$ be canonical and $\mathcal B\models T$. For each <closed term> $t$, define
$$
e(t^{\mathcal A})=t^{\mathcal B}.
$$
Every element of $A$ has a name, so this defines the desired map on all of $A$. If two <first-order terms> agree in $\mathcal A$, their <logical equality> <first-order sentence> holds in one <first-order model> of the <complete theory> and therefore in every <first-order model> of it; they agree in $\mathcal B$. This proves well-definedness. If they are distinct in $\mathcal A$, their inequality holds throughout the <complete theory> as well, proving <injectivity>.

For every <logical formula> $\phi(\vec x)$ and named <tuple> $\vec t^{\mathcal A}$, the substituted <first-order sentence> $\phi(\vec t)$ has the same <truth value> in the two <first-order models> by completeness of $T$. Consequently
$$
\mathcal A\models\phi(\vec t^{\mathcal A})\quad\Longleftrightarrow\quad
\mathcal B\models\phi(\vec t^{\mathcal B}).
$$
Thus $e$ is elementary. Since $\mathcal B$ was arbitrary, \b[every such <canonical first-order structure> is prime]. This <formal proof> also handles closed-term generation when <function symbols> are present; under the constant-name convention one simply uses constants as the <first-order terms>.