TU Vienna logic.at Theory and Logic Group (E185-2)

## Skolemization of Proofs

Skolemization is a transformation on closed formulas which removes all strong quantifiers. There are different types of skolemizations which may strongly differ in the proof complexity of the transformed formula (see [3]).

Definition 1
Let be a formula. If occurs positively (negatively) in then is called a strong (weak) quantifier. If occurs positively (negatively) in then is called a weak (strong) quantifier.

Below we define the structural skolemization operator defined in [4].

Definition 2
is a function which maps closed formulas into closed formulas; it is defined in the following way: if does not contain strong quantifiers, and

if is in the scope of the weak quantifiers (appearing in this order) and denotes after omission of and is a function symbol which does not occur in (if then is a constant symbol).

In model theory and automated deduction the definition of skolemization mostly is dual to Definition 2, i.e. in case of prenex forms the existential quantifiers are eliminated instead of the universal ones. The skolemization of sequents, defined below, represents a more general framework covering both concepts.

Definition 3
Let be the sequent consisting of closed formulas only and be the structural skolemization of . Then the sequent is called the skolemization of .

Example 1   Let be the sequent . Then the skolemization of is for a one-place function symbol and a constant symbol . Note that the skolemization of the left-hand-side of the sequent corresponds to the other skolemization concept for formulas mentioned above.

Not only formulas and sequents, but also whole proofs can be skolemized. By a skolemized proof we mean a proof of a skolemized end-sequent. Also proofs with cuts can be skolemized, but the cut formulas themselves cannot. Only the strong quantifiers which go'' into the end sequent are eliminated. Skolemization does not increase the length of proofs.

We do not give a formal definition of proof skolemization but refer to [4]. We merely give an example illustrating the transformation.

Example 2   Let

Then