Skolemization is refutation complete but not validation
complete. Means if you have a theory T, and its
skolemization T^S, you will know:
T |= [] iff T^S |= [].
This is why skolemization is often found in theorem
proving. For validity you would need Herbrandization
which will attack forall quantifiers and not existential
quantifiers. With Herbrandization one has:
[] |= T iff [] |= T^H
Both Skolemization and Herbrandization are based on
the following higher order identity and its dual
which can be obtained by negating both sides:
forall x exists y A(x,y) <-> exists f forall x A(x,f(x))
The identity makes use of the axiom of choice in one
direction. The quantification of the functorial f is
delegated to the signature of the first order theory
and the definition of the |= sign.
Possibly Skolemization and Herbrandization can be
combined, but I wouldn't confuse it with Morleyization
since both Skolemization and Herbrandization introduce
function symbols and not relation symbols.