Why does skolemization just happen under the scope of universal?

Question

I understand you can skolemize an existential under the scope of a universal and get :

$\forall$x $\exists$y.P(x,y) $\Leftrightarrow$ $\forall$x. P(x, f(x))

what if the universal quantifier is under the scope of negation? Can you get the following?

$\neg\forall$x $\exists$y.P(x,y)$\Leftrightarrow$ $\neg\forall$x. P(x, f(x))

As I understand skolemization usually is used in NNF, but why? what is wrong with the above?

my other question is how would you read this? $\neg\forall$x. P(x, f(x))

Answer 1

Welcome to MSE!

We skolemize so that we can find explicit witnesses to existential quantifiers. That is, if $\forall x . \exists y . P(x,y)$ we should be able to choose such a $y$ for each $x$. But a consistent way of making such a choice is exactly the function $f_P$ so that $\forall x . P(x, f_P x)$.

Let's think about what $\lnot \forall x . \exists y . P(x,y)$ says. It says that it isn't the case that every $x$ has such a $y$. Pushing to NNF, we can rewrite this as $\exists x . \forall y . \lnot P(x,y)$. That is, for some distinguished value of $x$, there is no choice of $y$ making $P(x,y)$ true.

Now I ask you, if we wanted to skolemize, what should $f_P(x)$ be? There's no choice of $y$ which makes $P(x,y)$ true. You ask in the question about the formula $\lnot \forall x . P(x,fx)$, and you certainly could consider a function which satisfies this equation. But it (probably) isn't a useful thing to study. Why?

The equation $\forall x. P(x,f_P x)$ determines the behavior of $f_P$. You can imagine there are very few $y$ for which $P(x,y)$, and so there aren't many choice of $f_P(x)$. In fact, this condition is strict enough to make skolemization a very useful procedure.

In contrast, what does the equation $\lnot \forall x. P(x,f_P x)$ tell us? Again, moving to NNF we see $\exists x . \lnot P(x, f_P x)$. But this tells us almost nothing! Indeed, to satisfy this formula, we only need to determine $f_P(x)$ for one choice of $x$. Moreover, we have almost free reign! If we again interpret $P(x,y)$ as being something which doesn't happen often, then almost any choice of $y$ will satisfy $\lnot P(x,y)$. So knowing that $f_P$ satisfies this condition gives very little control over $f_P$.

As for your last question, I've already answered it above. But explicitly, $\lnot \forall x . P(x,fx)$ should be read as

There is some $x$ which is not $P$ related to $fx$.

---

I hope this helps ^_^