= Skolem function
{c}
{title2=$f_\varphi$}
For each existential <first-order formula> $\exists y\,\varphi(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> satisfies
$$
\forall\mathbf x\bigl(\exists y\,\varphi(y,\mathbf x)\to\varphi(f_\varphi(\mathbf x),\mathbf x)\bigr).
$$
A 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.
Back to article page
