Skolem expansion (source code)

= Skolem expansion
{c}

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>.