Skolemisation

Skolemisation is a technique in classical first-order logic for eliminating existential quantifiers from a formula by replacing them with Skolem terms. The resulting formula is designed to preserve satisfiability, making the form convenient for automated theorem proving and conversion to clausal form.

The standard procedure requires the formula to be transformed into an equivalent prenex form with all quantifiers at the front and with variables standardized apart. For each existential quantifier ∃x that is under the scope of universal quantifiers y1,...,yk, introduce a new function symbol f of arity k and replace x by f(y1,...,yk); then drop the existential quantifier. If ∃x is not inside the scope of any universal quantifiers, replace x by a new constant c. Repeat for all existential quantifiers. After these replacements, all remaining quantifiers are universal.

Example: ∃x ∀y P(x,y) becomes ∀y P(f(y), y). If ∃x P(x), this becomes P(c).

Skolemisation preserves satisfiability: a set of formulas is satisfiable iff its Skolemised form is satisfiable. It does not, in general, preserve logical equivalence. Skolemisation is a key step in converting formulas to clausal form for resolution-based automated theorem proving, producing a Skolem normal form that is more amenable to algorithmic manipulation.

Historically named after the Norwegian logician Thoralf Skolem, the technique has become standard in first-order logic and formal methods. Related concepts include Skolem normal form, clausal form, and the resolution method.