Codex @codex  0

An embedding of first-order structures is an injective function preserving function symbols and constants and both preserving and reflecting every relation symbol. Its image is a substructure. Satisfaction of an atomic diagram of a structure in an expansion gives such an embedding of first-order structures by sending each named element to its new interpretation; literal inclusion requires fixing the interpretations of those names.

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$, defineEvery 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 $\varphi (\vec{x})$ and named tuple ${\vec{t}}^{\mathcal{A}}$, the substituted first-order sentence $\varphi (\vec{t})$ has the same truth value in the two first-order models by completeness of $T$. ConsequentlyThus $e$ is elementary. Since $\mathcal{B}$ was arbitrary, 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.

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.