In English, this formula says, "someone ($x$) is everybody's friend and nobody's foe". (Or, "someone is everybody's friend and has no foes", depending on how $Foe(a,b)$ is to read, and assuming is-a-foe-of is not symmetric – the question doesn't say. See comments below with @bof.) Note that you can rename the rightmost bound variable from $y$ to for example $z$, which may make it easier to figure out the meaning when you're first learning how to convert between ordinary language and first order formulas.
Converting it to prenex normal form is fairly straightforward. First, make sure that the bound variables are distinct, then move them across connectives. When a quantifier crosses a negation it changes from universal to existential and vice versa, as seen in step (2). Thus:
$$
\begin{align}
\exists x(\forall y Friend(x,y) \;\&\; \lnot (\exists y Foe(y,x))) &\iff \exists x(\forall y \,Friend(x,y) \;\&\; (\forall y \,\lnot Foe(y,x))) \tag{1}\\
&\iff \exists x(\forall y \,Friend(x,y) \;\&\; \forall y \,\lnot Foe(y,x)) \tag{2}\\
&\iff \exists x\forall y \,(Friend(x,y) \;\&\; \lnot Foe(y,x)) \tag{3}\\
\end{align}
$$
What each step does:
- $\lnot \exists y$ becomes $\forall y \,\lnot$
- Drop unneeded parentheses around right subformula
Coalesce universal quantifiers in conjoined subformulas into one universal quantifier around the entire conjunction: $$(\forall y\, p) \,\&\, (\forall y\, q) \iff \forall y\, (p \,\&\, q)$$
In fact the following is valid:
$$(\forall y\, p) \,\&\, (\forall z\, q) \iff \forall y\, (p \,\&\, q[z/y])$$
where $q[z/y]$ is the result of substituting $y$ for $z$ in $q$.
Two problems:
First, as Graham points out, going from
$$(\exists x \forall y \ r_1(x,g(y)) \lor \exists x \ \neg r_2(x,u))$$
to
$$\exists x \ ( \forall y \ r_1(x,g(y)) \lor \neg r_2(x,u))$$
is not an application of the Prenex laws
However, as it so happens, the existential does distribute over the disjunction, so you're lucky, and in fact this is a correct equivalence. But you'll have to justify it by 'Distribution of $\exists$ over $\lor$' rather than reference to Prenex laws. Or, as Graham suggests, first replace variables, and then use the Prenex Laws.
Second, going from
$$\exists x \ ( \forall y \ r_1(x,g(y)) \lor \neg r_2(x,u))$$
to
$$\forall y \exists x \ ( r_1(x,g(y)) \lor \neg r_2(x,u))$$
is a mistake. By the Prenex laws, the formula
$$\forall y \ r_1(x,g(y)) \lor \neg r_2(x,u)$$
is equivalent to:
$$\forall y ( r_1(x,g(y)) \lor \neg r_2(x,u))$$
and so, substituting that back, you get that:
$$\exists x \ ( \forall y \ r_1(x,g(y)) \lor \neg r_2(x,u))$$
is equivalent to
$$\exists x \ \forall y ( r_1(x,g(y)) \lor \neg r_2(x,u))$$
Best Answer
Close! Just a few small mistakes:
First, $\neg( \forall x. \exists y.P(x,y)))$ is equivalent to $\exists x. \neg \exists y.( P(x,y)))$, and thus to $\exists x. \forall y.\neg( P(x,y)))$
So, you end up with:
$(\exists u.\forall z.P(z,u) \wedge \exists x. \forall y.\neg P(x,y))$
and thus:
$\exists u.\forall z.\exists x. \forall y.(P(z,u) \wedge \neg P(x,y))$
Second, whenever you are Skolemizing, you should pay attention to any existentials that come after any universals. Consider the following:
$\forall x.\exists y.S(y,x)$
where $S(y,x)$ means '$y$ is the successor of $x$'. Now, if this is about whole numbers, then it is clear that this is a true statement: For every number there is a successor. But also note that there is not one number that is the successor to all numbers. So, there is no constant $a$ such that
$\forall x.S(a,x)$
is true. So that is not what you want as the Skolemization of the statement. Instead, notice that the successor of a number $x$ depends on what the number $x$ is. Indeed, we can think of this as a function from $x$ to $y$. So, what we can say, is that there is some function $f$ such that
$\forall x.S(f(x),x)$
is true. And that is exactly what the correct Skolemization is (make sure that $f$ is a 'new' function, i.e. not a function symbol that is used anywhere else in your statement(s) under consideration)
So, the Skolemization of your original statement:
$\exists u.\forall z.\exists x. \exists y.(P(z,u) \wedge \neg P(x,y))$
should have been:
$\forall z.(P(z,a) \wedge \neg P(f(z),g(z)))$
And applied to the corrected:
$\exists u.\forall z.\exists x. \forall y.(P(z,u) \wedge \neg P(x,y))$
you get:
$\forall z. \forall y.(P(z,a) \wedge \neg P(f(u),y))$
One last thing. In this particular case, you can actually avoid the use of such a function. Let's go back to:
$(\exists u.\forall z.P(z,u) \wedge \exists x. \forall y.\neg P(x,y))$
Here, we can first take out the $\exists u$, then the $\exists x$, then the $\forall z$, and finally the $\forall y$, resulting in:
$\exists u.\exists x.\forall z. \forall y.(P(z,u) \wedge \neg P(x,y))$
And now, when you Skolemize, you simply get:
$\forall z. \forall y.(P(z,a) \wedge \neg P(b,y))$