Elementary substructure ($M\prec N$)

A substructure $M\subseteq N$ is elementary when every first-order formula with parameters from $M$ has the same truth value in $M$ and $N$.

An injective map between subsets of structures is partial elementary when it preserves every first-order formula on tuples from its domain. This is stronger than a partial embedding, which only preserves quantifier-free formulas. In countable models, successive one-point extensions in both directions produce an elementary isomorphism by the back-and-forth method.

A substructure $M\subseteq N$ is elementary if and only if, whenever $N\models \exists x\phi (x,\bar{a})$ with parameters $\bar{a}$ from $M$, some witness $b\in M$ satisfies $N\models \phi (b,\bar{a})$.

The witness criterion characterizes an elementary substructure, and hence preservation of all first-order formulas with parameters from the substructure.

After choosing a Skolem function for each existential formula, the Skolem hull of $A\subseteq N$ is the smallest subset containing $A$ and closed under those functions. The Tarski-Vaught test makes it an elementary substructure of $N$, and in a countable language an infinite hull has cardinality at most $|A|+{\aleph }_0$.

For each existential first-order formula $\exists y\phi (y,\mathbf{x})$ in a structure, a Skolem function selects a witness when one exists, with an arbitrary default when none exists. An expansion containing these functions satisfiesA subset closed under all such functions is elementary in the original language by the Tarski-Vaught test. Simultaneously choosing these functions is performed in the ordinary classical metatheory with choice.

Replacing an existentially quantified variable by a fresh Skolem function of the preceding universally quantified variables. A witness independent of all universal variables is represented by a fresh constant. The operation preserves satisfiability after expanding the first-order signature; it is not generally logical equivalence for arbitrary interpretations of the new symbols.

A first-order sentence consisting of a block of universal quantifiers followed by a quantifier-free formula, obtained by Skolemization in an expanded first-order signature. Its matrix can additionally be put into conjunctive normal form to obtain clausal form.

A Skolem expansion adjoins a Skolem function for every existential first-order formula. Iterating through the successively enlarged languages, and taking their union, gives a language with witness functions even for first-order formulas involving previously added functions. Starting from a language of size $\kappa$, the resulting language has size at most $\kappa +{\aleph }_0$. A hull closed under its functions is a Skolem hull and is elementary in the expanded structure by the Tarski-Vaught test.