Why does Skolemming not preserve validity?
When the existentials that are being removed in the process of Skolemization are not preceded y universals, you simply use a new constant for the respective variables.
As such, consider the formula:
$$\exists x (P(a) \lor \neg P(x))$$
This is a valid formula, since in any domain there is always an object that will satisfy the formula $P(a) \lor \neg P(x)$, namely whatever object $a$ refers to.
However, if we Skolemize, we get:
$$P(a) \lor \neg P(b)$$
which is not a valid formula, since there is a domain and interpretation where this statement is false: make sure that $a$ and $b$ refer to different objects, and where the object that $a$ refers to does not have the property expressed by $P$, while the object referred to by $b$ does have that property.
A sentence is valid if it is true in every interpretation of its logical language.
A sentence is satisfiable if it is true in some interpetation of its logical language.
Since Skolemization adds new symbols to the logical language, I think it is useful to introduce concepts of relative validity and satisfiability:
Suppose $\mathcal L\subseteq \mathcal L'$ are logical languages, and $\mathfrak A$ is an interpretation of $\mathcal L$. Then,
- An $\mathcal L'$-sentence is valid relative to $\mathfrak A$ if it is true in every extension of $\mathfrak A$ to an interpretation of $\mathcal L'$.
- An $\mathcal L'$-sentence is satisfiable relative to $\mathfrak A$ if it is true in some extension of $\mathfrak A$ to an interpretation of $\mathcal L'$.
(Beware that "relative" validity and satisfiability is probably not standard terminology; I made it up for the purpose of this explanation).
Now, when we Skolemize an $\mathcal L$-sentence $\varphi$, we get an extended language $\mathcal L'\supseteq \mathcal L$ and an $\mathcal L'$-sentence $\varphi'$. This trades truth for satisfiability in the sense that
For every interpretation $\mathfrak A$ of $\mathcal L$ it holds that $\varphi$ is true in $\mathfrak A$ if and only if $\varphi'$ is satisfiable relative to $\mathfrak A$.
In other words, if $\varphi$ is true in $\mathfrak A$, then we can find some interpretation of the Skolem functions that makes $\varphi'$ true, and vice versa. But we have no guarantee that every possible interpretation of the Skolem functions will preserve the truth of $\varphi$ -- indeed, usually they won't (as Bram28's counterexample shows).
This means that if we just have $\varphi$ and is not looking at a particular $\mathfrak A$, the Skolemization preserves validity:
- $\varphi$ is satisfiable $\iff$
- There is some interpretation of $\mathcal L$ where $\varphi$ is true $\iff$
- There is some interpretation of $\mathcal L$ which extends to some interpretation of $\mathcal L'$ where $\varphi'$ is true $\iff$
- There is some interpretation of $\mathcal L'$ where $\varphi'$ is true $\iff$
- $\varphi'$ is satisfiable.
If we try to replicate this argument with "valid" instead of "satisfiable", we get stuck after step 3:
- Every interpretation of $\mathcal L$ extends to some interpretation of $\mathcal L'$ where $\varphi'$ is true.
Whereas the original (3) had two "some" that we could collapse to one in (4), here we have a combination of "every" and "some". And that cannot be collapsed to a simple statement about interpretations of $\mathcal L'$ and $\varphi'$ -- in particular it is not equivalent to $\varphi'$ being valid.