How do I transform the following formula into prenex normal form without using more quantifiers than necessary?
$$\exists x(\forall y\; \operatorname{Friend}(x,y) \;\& \;\lnot (\exists y\; \operatorname{Foe}(y,x)))$$
I have looked at all of the laws around how to go about putting such formulas in prenex normal forms such as the Conjunction and Disjunction rules, however I can't find any that seem to fit.
Best Answer
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:
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$.