Solution (source code)

= Solution

A <model companion> $T^*$ of a <first-order theory> $T$, in the same <first-order language>, is a <model-complete theory> with the same <universal consequences of a theory> as $T$:
$$
\boxed{T^*\text{ is model-complete and }T^*_\forall=T_\forall.}
$$
Equivalently, every model of $T$ embeds into a model of $T^*$, and every model of $T^*$ embeds into a model of $T$. The equivalence follows from the <diagram embedding criterion for universal theories>, which is an application of the <compactness theorem>. A <model companion> need not be a syntactic extension of $T$, and uniqueness is understood up to logical equivalence of theories.