Model companion (source code)

= Model companion
{title2=$T^*$}
{wiki}

A model companion of $T$ is a <model-complete theory> $T^*$ in the same language with $T^*_\forall=T_\forall$. Equivalently each model of either theory embeds into a model of the other. Alternating these embeddings and using the <elementary chain theorem> proves uniqueness up to logical equivalence. A model companion need not be a syntactic extension of its original theory.