Suppose we are given a proof task of the form

A, (X)(y)(W)B [] Qwhere A is some set of formulae, where W is some sequence of quantifiers, where B is a formula that does not begin with a quantifier, and where [] indicates that the signature involved is .

Then to achieve this proof task, it suffices to do the proof task

A, (X)(W)P' [(y')] Qwhere [](y') indicates the signature formed from [] by adding a new function symbol y', called a

This rule, called **Skolemization** (after the
logician Thoralf Skolem) is justified in Chapter 8 of *Theorem Proving and
Algebra*.

For example, given the proof task (where the variables range over integers)

(x)(y)(x + y = 0) [] Q .it suffices to prove

(x)(x + y'(x) = 0) [(y')] Q .where y'(x) is the Skolem function (it is the negation function in this case). In many cases the Skolemized form is easier to use.

This rule can be applied repeatedly to eliminate all existential quantifiers from formulae to the left of the symbol.

[Prev] [Home] [BHome]

12 March 1998