HLK ProofTool
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 $B$ be a formula. If $(\forall x)$ occurs positively (negatively) in $B$ then $(\forall x)$ is called a strong (weak) quantifier. If $(\exists x)$ occurs positively (negatively) in $B$ then $(\exists x)$ is called a weak (strong) quantifier.

Below we define the structural skolemization operator ${\it sk}$ defined in [4].

Definition 2  
${\it sk}$ is a function which maps closed formulas into closed formulas; it is defined in the following way: ${\it sk}(F) = F$ if $F$ does not contain strong quantifiers, and

\begin{displaymath}
{\it sk}(F) = {\it sk}(F_{(Qy)} \{y\leftarrow f(x_1,\ldots ,x_n)\})
\end{displaymath}

if $(Qy)$ is in the scope of the weak quantifiers $(Q_1x_1),\ldots,(Q_nx_n)$ (appearing in this order) and $F_{(Qy)}$ denotes $F$ after omission of $(Qy)$ and $f$ is a function symbol which does not occur in $F$ (if $n=0$ then $f$ 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 $S$ be the sequent $A_1,\ldots ,A_n \vdash B_1,\ldots, B_m$ consisting of closed formulas only and $(A_1'\wedge \ldots \wedge A_n') \to (B_1'\vee \ldots \vee B_m')$ be the structural skolemization of $(A_1\wedge \ldots \wedge A_n)\to
(B_1\vee \ldots \vee B_m)$. Then the sequent $S':A_1',\ldots ,A_n'\vdash
B_1',\ldots ,B_m'$ is called the skolemization of $S$.

Example 1   Let $S$ be the sequent $(\forall x)(\exists y)P(x,y) \vdash (\forall x)(\exists
y)P(x,y)$. Then the skolemization of $S$ is $S':\ (\forall
x)P(x,f(x)) \vdash (\exists y)P(c,y)$ for a one-place function symbol $f$ and a constant symbol $c$. 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 ${\it sk}$ but refer to [4]. We merely give an example illustrating the transformation.

Example 2   Let $\varphi =$

\begin{displaymath}
\infer=[\forall :l]{(\forall x)P(c,x), (\forall x)(\exists y...
...dash P(c,\alpha)
&
Q(\alpha) \vdash Q(\alpha)
}
}
}
}
}
\end{displaymath}

Then ${\it sk}(\varphi ) =$

\begin{displaymath}
\infer=[\forall :l]{(\forall x)P(c,x), (\forall x)(P(x,f(x))...
...,f(c)) \vdash P(c,f(c))
&
Q(f(c)) \vdash Q(f(c))
}
}
}
}
\end{displaymath}