4
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

"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).

$\endgroup$
1
$\begingroup$

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))$.

$\endgroup$
  • $\begingroup$ Helpful demonstration of the limits of equisatisfiability. I assume that this means that the accepted answer is correct and you can always de-Skolemize inferences derived from Skolemized sentences? $\endgroup$ – dezakin Oct 19 '14 at 17:10
  • $\begingroup$ No. The second order identity ∀x∃y ϕ(x,y) ⟺ ∃F∀x ϕ(x,F(x)) which means ∃x∀y∃zϕ(x,y,z) ⊢ ∃F∀xϕ(a,x,F(x)). From ∃F∀xϕ(a,x,F(x)) we detach the second order existential quantifier for a satisfiable first order statement ∀xϕ(a,x,F(x)) where F satisfies some model. We can restore the second order existential quantifier after making inferences to return from a satisfiable to true, and use the original identity to de-skolemize and restore the statement to a bound first order sentence. $\endgroup$ – dezakin Oct 19 '14 at 21:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.