I'm wondering what exactly is meant when people say "Skolemization preserves satisfiability but not validity". I'm having trouble wrapping my brain around it because I think of Skolemization, when considered as an inference rule, to simply "be an okay thing to do" when working with a second-order formula.
Skolemization is said to preserve satisfiability but not validity. What exactly do satisfiability and validity mean in the context? Does "co-Skolemization" (dual to Skolemization as a second-order equivalence) have similar properties as Skolemization?
Skolemization, as far as I can tell, is based on the equivalence between the first-order formula (and therefore degenerate second-order formula)
$$ \forall x_1 \cdots x_n . \exists y . P(x_1, \cdots, x_n, y) $$
and the following second order formula, that moves the $\exists$ in front of the $\forall$.
$$ \exists f. \forall x_1 \cdots x_n . P(x_1, \cdots, x_n, f(x_1, \cdots, x_n))$$
It makes perfect sense when the expression is thought of as a game. In the first expression, the opponent first makes $n$ moves and then the player makes 1. In the second expression, the player moves first but commits to a response function of sorts rather than committing to a single move. That's not a proof, but it seems like good intuitive justification for why rewriting an expression like this is okay in the first place.
It seems to me that performing this translation at all only makes sense if we're talking about a closed expression. That is, $P(\cdots)$ must have no free variables or, equivalently, $P$ must be an $n+1$-place predicate (primitive or defined).
In propositional logic, satisfiability and validity can be though of as describing what happens to free variables. All variables are free because there's no way to bind them.
$ P \lor P $ is satisfiable because the assignment $ \{ P = \top \} $ satisfies it.
$ P \lor \lnot P $ is a tautology for obvious reasons. I don't know whether it's right to say $ P \lor \lnot P $ is valid.
An inference rule that maps $P$ to $P \lor Q$ is valid (disjunction introduction).
A rule that maps $P$ to $P \land Q$ preserves satisfiability. We can take any old assignment $\mu$ and construct $\mu \cup \{ Q = \top \}$ which satisfies the new expression.
In the context of Skolemization, are the meanings of satisfiability and validity similar?
Let "co-Skolemization" (probably has a real name) be the translation from
$$ \exists x_1 \cdots x_n . \forall y . P(x_1, \cdots, x_n, y) $$
to
$$ \forall f . \exists x_1 \cdots x_n . P(x_1, \cdots, x_n, f(x_1, \cdots, x_n)) $$
That seems just as legitimate as Skolemization, considered as an inference rule in a second-order setting. There's a caveat here that in a first-order theory definitions are provided for all fully saturated combinations of function symbols and arguments. Therefore "co-Skolemization" definitely takes us out of first-order land, but I don't know how relevant that is.
Best Answer
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.