Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2008 / B / 6 / ii / Solution

If $\mathcal{A}\subseteq \mathcal{B}$, interpret each new constant $c_a$ in $\mathcal{B}$ as the same element $a$. Atomic logical formulas and their negations then have exactly their truth values in ${\mathcal{A}}_A$, so the expansion satisfies the diagram of a structure. If the inclusion is elementary, every logical formula with those named parameters has the same truth value, so the expansion satisfies the elementary diagram.

Conversely, from any expansion ${\mathcal{B}}^{+}$ satisfying the diagram of a structure defineThe diagram of a structure contains $c_a\ne c_{a^{\prime }}$ whenever $a\ne a^{\prime }$, so $e$ is injective. It contains every true function-value equation, so $e$ commutes with all operations and constants. Positive and negative relation instances ensure both preservation and reflection of the relations. Thus $e$ is an embedding of first-order structures. If the expansion satisfies the elementary diagram, for every logical formula $\varphi$ and tuple $\vec{a}$ it also givesso $e$ is an elementary embedding of first-order structures.

The precise conclusion for an arbitrary expansion is an embedding of first-order structures, rather than a literal inclusion of the original carriers. The source's inclusion notation is correct when one uses the customary identification of $\mathcal{A}$ with its embedded copy, or requires the expansion to interpret $c_a$ as the actual element $a$ of a carrier already containing $A$. With that naming convention, $e$ is the inclusion and the requested two equivalences follow exactly.

Without the convention the literal wording fails, even in the first-order language of logical equality: singleton first-order structures with carriers $\{0\}$ and $\{1\}$ have a diagram-satisfying expansion by sending the first first-order structure's named point to $1$, but the first carrier is not a subset of the second. The embedding of first-order structures formulation proved above states the invariant result and makes the intended inclusion formulation precise.