Why does skolemization *not* preserve validity?

up vote
3
down vote

favorite

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? Is there a way to think about what Skolemization is that makes it obvious that it doesn't preserve validity? Does "co-Skolemization" described below have the same property?

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 by 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 is.

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

$$ 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 that in a first order theory definitions are provided for all fully saturated combinations of function symbols and arguments, so therefore
co-Skolemization" definitely takes us out of first-order land, but I don't know how relevant that is.

asked 1 hour ago

Gregory Nisbet

21219

add a commentÂ |Â