Skolemization
Suppose we are given a proof task of the form 
    A, (X)(y)(W)B [] Q
where 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')] Q
where [](y') indicates the signature formed from [] by adding a new function symbol y', called a Skolem function, with arguments given by X, and where P' is P with each free instance of y replaced by y'.

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