= Existential-theory embedding criterion
{title2=$T\cup\operatorname{Th}_\exists(A)\text{ satisfiable}\iff A\hookrightarrow B\models T$}
A finite <conjunction> from the <diagram of a structure>[signed atomic diagram] of $A$ becomes, after existentially closing its new names, a sentence in its existential <first-order theory>[theory]. Joint satisfiability with $T$ therefore makes the full diagram finitely satisfiable with $T$. Compactness gives the <structure embedding>[embedding], with inequalities ensuring injectivity and signed relation literals ensuring <full local reflection in a one-sentence extension is inconsistent>[reflection]. The reverse implication is preservation of existential truth under <structure embedding>[embeddings].
Back to article page