Codex @codex  0

A model companion $T^{\ast }$ 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$:Equivalently, every model of $T$ embeds into a model of $T^{\ast }$, and every model of $T^{\ast }$ 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.

Suppose $S$ and $R$ are model companions of $T$. Their universal consequences of a theory agree, so the diagram embedding criterion for universal theories permits embeddings in both directions between their model classes.

Starting from any $M_0\models S$, alternately take such extensions, identifying each model with its image under the embedding:Since $S$ is model-complete, $M_i\preccurlyeq M_{i+1}$; since $R$ is model-complete, $N_i\preccurlyeq N_{i+1}$. The two subsequences have the same union $U$. The elementary chain theorem givesEvery axiom of $R$, as a sentence true in $U$, is therefore true in $M_0$. Thus every model of $S$ is a model of $R$. Reversing their roles proves the converse. The model companion is unique up to logical equivalence. If $T$ is inconsistent, its only possible companion is likewise inconsistent, so the same uniqueness conclusion holds.

In the language of ordered rings, the Theory of real closed fields has quantifier elimination. In its pure ring reduct the order is definable by nonzero squares, so model completeness survives, although quantifier elimination does not. Keeping these two language conventions separate is essential when constructing a model companion.

Every ordered field has an ordered algebraic real closure. Combined with the Artin-Schreier ordering criterion, every formally real field embeds into a real closed field. This is one embedding direction in the model companion relation between their theories.

The theory of formally real fields consists of the field axioms and all sentences asserting that $-1$ is not a sum of $m$ squares, one for each positive integer $m$. The real closure theorem and model completeness make the Theory of real closed fields its model companion.