= 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> define
$$
e:A\to B,\qquad e(a)=c_a^{\mathcal B^+}.
$$
The <diagram of a structure> contains $c_a\ne c_{a'}$ whenever $a\ne a'$, 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> $\phi$ and <tuple> $\vec a$ it also gives
$$
\mathcal A\models\phi(\vec a)\quad\Longleftrightarrow\quad
\mathcal B\models\phi(e(\vec a)),
$$
so $e$ is an elementary <embedding of first-order structures>.
\b[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.
Back to article page
