Method of diagrams

The method of diagrams adds the diagram or elementary diagram of a structure to a theory and applies compactness. A resulting model supplies an embedding or elementary embedding of the named structure.

A first-order structure $A$ embeds into a model of $T$ exactly when $A\models T_{\forall }$. For the nontrivial direction apply the compactness theorem to $T\cup \mathrm{Diag}(A)$. If a finite diagram conjunction were inconsistent with $T$, its universal negation after replacing the new constants by variables would belong to $T_{\forall }$ and contradict its truth in $A$.

If a type $p(x)$ over a structure $M$ is finitely satisfiable in $M$, then the elementary diagram of $M$ together with $p(c)$ is finitely satisfiable. Compactness gives an elementary extension of $M$ realizing $p$.