Skolemization

Skolemization step

2

4

6

8

10

arithmetical level

Σ : existential

Π : universal

alternations

1

2

3

repeating quantifiers

1

2

free variable

yes

no

initial formula:

∃

x1

∀

x2

∃

x3

P(x1,x2,x3)x3

The process of removing all the existential quantifiers from a formula is known as Skolemization. The result is a formula in Skolem normal form that is equivalent in computational complexity to the original. This Demonstration shows the rewriting process of a Skolemization step by step for all general cases up to three quantifier alternations and seven variables or constants.