A model companion of a first-order theory , in the same first-order language, is a model-complete theory with the same universal consequences of a theory as :
Equivalently, every model of embeds into a model of , and every model of embeds into a model of . 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 , and uniqueness is understood up to logical equivalence of theories.
Suppose and are model companions of . 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 , alternately take such extensions, identifying each model with its image under the embedding:
Since is model-complete, ; since is model-complete, . The two subsequences have the same union . The elementary chain theorem gives
Every axiom of , as a sentence true in , is therefore true in . Thus every model of is a model of . Reversing their roles proves the converse. The model companion is unique up to logical equivalence. If is inconsistent, its only possible companion is likewise inconsistent, so the same uniqueness conclusion holds.
The universal consequences of a first-order theory are all universal first-order sentences entailed by . Their model class is exactly the class of substructures of models of , up to structure embedding. This characterization follows from the diagram embedding criterion for universal theories.