When is de-Skolemizing statements appropriate?

Question

In first order logic we often convert prenex normal form statements to Skolem normal form statements to eliminate the existential quantifier:

$\exists$x$\forall$y$\exists$z$\phi$(x,y,z) becomes

$\forall$x$\phi$(a,x,f(x))

Where a is a 'Skolem constant' and f is a 'Skolem function'

Because we remove all the existential quantifiers, we can drop all quantifiers and consider all variables implicitly universally quantified and perform inferences more freely.

This makes things easier for refutation based automated theorem proving. Since Skolem normal form is equisatisfiable to prenex normal form, this is entirely appropriate for refutation; we go down the chain of inferences until we either saturate the search and prove satisfiability, or we run into a contradiction and prove unsatisfiability, and thus validity of the negation of the statement in question.

Can we use use Skolemization for non-refutation theorem proving? The problem I'm concerned about is Skolem normal form is equisatisfiable, but not equivalent, to prenex normal form. Proving a theorem with refutation only requires equisatisfiability, but I'm not sure if that's enough for regular inferences.

If I have the statement:

$\exists$x$\forall$y$\exists$z$\phi$(x,y,z) becomes $\forall$x$\phi$(a,x,f(x))

$\phi$(a,x,f(x)) $\vdash$ $\psi$(a,x,f(x))

Does that always imply

$\exists$x$\forall$y$\exists$z$\psi$(x,y,z)?

If I perform inferences on a Skolemized statement, can I always 'de-Skolemize' the Skolem constants and Skolem functions?

Answer 1

"If I have the statement:

∃x∀y∃zϕ(x,y,z) becomes ∀xϕ(a,x,f(x))

ϕ(a,x,f(x)) ⊢ ψ(a,x,f(x))

Does that always imply

∃x∀y∃zψ(x,y,z)?"

Suppose that we have ϕ(a,x,f(x)), and ϕ(a,x,f(x)) ⊢ ψ(a,x,f(x)). We can then detach ψ(a,x,f(x)). The Wikpedia on Skolemization indicates that it works, because of equivalences:

"Skolemization works by applying a second-order equivalence in conjunction to the definition of first-order satisfiability. The equivalence provides a way for "moving" an existential quantifier before a universal one."

Thus we just use the equivalences "in the other direction" and we end up with ∃x∀y∃zψ(x,y,z).

Answer 2

This is a long comment ...

Regarding your question, we have to note that :

if $\varphi := ∀x∃y \psi(x,y)$ and $\varphi^S := ∀x \psi(x,f(x))$ is its skolemization, then $\varphi \nvdash \varphi^S$,

as per Andreas' answer to this post, while they are equisatisfiable.

Andreas gives a semantic argument; here is a proof-theoretic one, based on Natural Deduction.

---

Consider the language of first-order arithmetic. In it we have :

• (individual) variables : $x,y,\ldots$;

• an individual constant : $0$;

• an unary function symbol : $S$ for the "successor" function;

• two binary function symbols : $+$ and $\times$, for the operations of "sum" and "product" respectively.

With them, we can build terms. The following :

$x, 0, S(x), S(0), x+x, x+0, x+S(0), x+S(y), \ldots$

are terms of first-order arithmetic.

Consider as $\varphi$ the formula :

$\forall x \exists y (x < y)$;

its skolemization $\varphi^S$ is :

$\forall x(x < S(x))$.

The two formulae are both true with the "standard" interpretation with domain $\mathbb N$, and thus they are equisatisfiable (i.e. both have a model).

An attempted proof of $\varphi \vdash \varphi^S$ have to use the rule for $\exists$-Elimination; see Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), page 179 :

if $\Gamma, \varphi[t/y] \vdash \chi$, then $\Gamma,∃y \varphi \vdash \chi$, provided that $t$ is a constant symbol or a variable which does not occur in $\chi, \varphi$ or any formula of $\Gamma$, except $\varphi[t/y]$.

Consider now our example :

(1) $\forall x \exists y (x < y)$ --- premise (it is the only formula in $\Gamma$)

(2) $\exists y (x < y)$ --- from (1) by $\forall$E

(3) $(x < S(x))$ --- assumed [a] for $\exists$E from (2) --- illegal !

$y$ is not free in $\Gamma$, i.e. in (1); thus we can apply $\exists$E to derive :

(4) $(x < S(x))$ --- from (2), discharging assumption [a]

(5) $\forall x (x < S(x))$ --- from (4) by $\forall$I, $x$ is not free in $\Gamma$.

The conclusion is true, but the derivation is incorrect, because in step (3) we have used for $\exists$E a term : $S(x)$ which is not a variable or constant.

The proviso is necessary, in order to prevent fallacies; if the use of a term whatever is licensed in the application of the $\exists$E rule, we can repeat the above derivation with $x+0$ in place of $S(x)$, and we will get :

$\forall x \exists y (x < y) \vdash \forall x (x < x+0)$

which is clearly false in $\mathbb N$.

---

The conclusion is, for $\varphi$ and its skolemization $\varphi^S$, that :

$\varphi \nvdash \varphi^S$

and so :

$\varphi \nvDash \varphi^S$.

Thus, in your proof starting from : $∃x∀y∃zϕ(x,y,z)$, you have to note that you are not licensed to assume that $∃x∀y∃zϕ(x,y,z) \vdash∀xϕ(a,x,f(x))$.