Solution (source code)

= Solution

If a <first-order model>[model] $B$ of $T$ contains $A$ as a <substructure of a first-order structure>[substructure], every <existential sentence> true in $A$ remains true in $B$: use the same witness tuple and preservation of quantifier-free truth. Hence $B$ satisfies the required joint <first-order theory>[theory].

For the <existential-theory embedding criterion>, conversely suppose that joint <first-order theory>[theory] has a <first-order model>[model]. Expand the language by a constant $c_a$ for each $a\in A$, and add the atomic and negated <diagram of a structure>[atomic diagram] $D(A)$ to $T$. Any finite collection of its literals is a quantifier-free <conjunction> $\theta(\bar c)$ true of the corresponding tuple in $A$. Replacing those named constants by variables and existentially closing gives a sentence in $\operatorname{Th}_\exists(A)$. A <first-order model>[model] of the assumed joint <first-order theory>[theory] can supply its witnesses, and hence an expansion satisfying those finitely many diagram requirements and any finite <subset> of $T$.

Compactness therefore gives a <first-order model>[model] of $T+D(A)$. Its named <Elements> define an <structure embedding>[embedding] of $A$ into its $L$-reduct: inequalities ensure injectivity, and all function and relation literals ensure preservation and <full local reflection in a one-sentence extension is inconsistent>[reflection]. Replace the ambient <first-order model>[model] by an isomorphic copy identifying this image with $A$ itself. Thus \b[a <first-order model>[model] of $T$ containing $A$ exists]. The diagram step explains how parameter-free existential information nevertheless yields an <structure embedding>[embedding] of the whole structure.