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?