= Diagram embedding criterion for universal theories
{title2=$A\models T_\forall\iff A\hookrightarrow N\models T$}
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\operatorname{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$.
Back to article page
