The process of eliminating existential quantifiers in a sentence in prenex normal form, i.e., a sentence of the form

• • ${\text{Q}}_0{x}_0...{\text{Q}}_{n-1}{x}_{n-1}\phi$

where each ${\text{Q}}_i$ is a quantifier and $\phi$ (the matrix) is quantifier free, by introducing constants and function symbols (so-called Skolem constants and Skolem functions). The process of producing a Skolem normal form of a formula $\psi$ proceeds recursively by applying the following step until no existential quantifiers remain in the formula:

• • For the existential quantifier ${\exists }_j{x}_j$ with the least index (i.e., the leftmost instance of ${\exists }_j{x}_j$) that follows a string of $m$ universal quantifiers ${\forall }_{k_0}{x}_{k_0}...{\forall }_{k_{j-1}}{x}_{k_{m-1}}$ (possibly empty), the quantifier ${\exists }_j{x}_j$ is deleted and each instance of $x_j$ in the matrix is replaced by a Skolem function $f_j\left(x_{k_0},...,x_{k_{m-1}}\right)$, where $f_j$ is a new function symbol.

If $\exists x_j$ is not within the scope of any universal quantifier, then $f_j$ is nullary, i.e., a Skolem constant $c_j$. The formula ${\psi }^{\prime }$ that ensues after finitely many applications of this scheme is the Skolem normal form of $\psi$. For example, two applications of the above scheme turns the formula

• • $\forall x_0\exists x_1\exists x_2\forall x_3\exists z\phi \left(x_0,x_1,x_2,x_3\right)$

into its Skolem normal form:

• • $\forall x_0\forall x_3\exists z\phi \left(x_0,f_1\left(x_0\right),f_2\left(x_0\right),x_3\right)$

While $\psi$ and ${\psi }^{\prime }$ are not logically equivalent in classical logic, they are equisatisfiable in the sense that $\psi$ has a model if and only if ${\psi }^{\prime }$ has a model. Equisatisfiability of $\psi$ and its Skolem normal form is sufficient for the task for which it was defined, i.e., in the proof of the Löwenheim-Skolem theorem by its namesake, mathematician Thoralf Skolem (1887–1963), according to which any satisfiable formula $\phi$ has a countable model.