Prenex form of an expression: Cannot understand example

Question

My new course in this semester starts of with predicate-logic and on the way touches prenex form, quantifiers, skolemization and unification - all topics quite new for me. I do not start completely from scratch but with little previous knowledge.

For homework I need to solve an expression and noticed I barely understand the topic.

The first step in my assignment is finding the (better: a?) prenex form of the equation. I did study my schools script but it does not contain much information about the rules to manipulate quantized expressions so I researched more lecture material of others faculties. That helped a lot, but also brought me to an example I cannot grasp:

On page 134 of this PDF (that's page 148 in pdf pages) you find example 4.58 like this: $$ 1. \; \; \; ∀y \; (∀x \; ∀y \; p(x,y) → \; ∃x r(x,y)) \\ 2. \; \; \; ∀y \; (∀x \; ∀z \; p(x,z) → \; ∃u r(u,y)) \\ 3. \; \; \; ∀y \; ∃x \; (∀z \; p(x,z) → \; ∃u r(u,y)) \\ 4. \; \; \; ∀y \; ∃x \; ∃z \; (p(x, z) → \; ∃u r(u,y)) \\ 5. \; \; \; ∀y \; ∃x \; ∃z \; ∃u \; (p(x, z) → r(u,y)) $$ I do understand line 1 to line 2: name conflict in x and y is resolved by renaming y to z and x to u.

But line 2 to 3, and line 3 to 4 are a mystery to me. Why does pulling out the "all x" change it to an "at least one x"? Same question for line 3 to 4, why does "all z" become a "one z"?

On the same page, above this example, there is an example mentioning that more than one prenex form can be transformed out of an equation $$ ∀x\;p(x) → ∀y\;q(y) $$ can be transformed to $$ ∃x\;∀y\;(p(x) → q(y)) $$ as well as $$ ∀y\;∃x\;(p(x) → q(y)) $$ both of which I do not understand at all. Why doesn't it give $$ ∀x\;∀y\;(p(x) → q(y)) $$

Thanks for your help. I will post at least two other question regarding this homework assignment and relate them together as soon as they are posted.

Answer 1

Prenex normal form basically is exploiting the following transforms (some of which require the standard non empty universe caveat):

$$B \land \forall x ~ A(x) = \forall x ~ (B \land A(x))$$ $$B \lor \forall x ~ A(x) = \forall x ~ (B \lor A(x))$$ $$B \land \exists x ~ A(x) = \exists x ~ (B \land A(x))$$ $$B \lor \exists x ~ A(x) = \exists x ~ (B \lor A(x))$$ $$ \lnot \exists x ~ A(x) = \forall x ~ \lnot A(x)$$ $$ \lnot \forall x ~ A(x) = \exists x ~ \lnot A(x)$$

So when converting to prenex, just write your equations as $\land$, $\lor$, and $\lnot$ and use the above transforms.

$$2. \quad \forall y ~ (\forall x ~ \forall z ~ p(x,z) \implies \exists u~ r(u,y))$$

Rewrite the $\implies$ using $\lor$ and $\lnot$ :

$$\forall y ~ \boxed{ \boxed{\forall x \boxed{\forall z ~p(x,z)}} \implies \boxed{\exists u~ r(u,y)} }$$

$$\forall y ~ \boxed{ \lnot \boxed{\forall x \boxed{\forall z ~p(x,z)}} \lor \boxed{\exists u~ r(u,y)} }$$

Now use $ \lnot \forall x ~ A(x) = \exists x ~ \lnot A(x)$ a couple times to put the $\lnot$ inside of quantifiers:

$$\forall y ~ \boxed{ \boxed{ \exists x \lnot \boxed{\forall z ~p(x,z)}} \lor \boxed{\exists u~ r(u,y)} } \tag{A}$$

$$\forall y ~ \boxed{ \boxed{ \exists x \boxed{\exists z ~\lnot p(x,z)}} \lor \boxed{\exists u~ r(u,y)} }$$

Now use $B \lor \exists x ~ A(x) = \exists x ~ (B \lor A(x))$ a bunch of times to put the $\lor$ inside of quantifiers:

$$\forall y ~ \boxed{ \exists x \boxed{ \boxed{\exists z ~\lnot p(x,z)} \lor \boxed{\exists u~ r(u,y)} }} \tag{T}$$

$$\forall y ~ \boxed{ \exists x \boxed{\exists z \boxed{~\lnot p(x,z) \lor \boxed{\exists u~ r(u,y)} }}} \tag{C}$$

$$\forall y ~ \boxed{ \exists x \boxed{\exists z \boxed{ \boxed{\exists u~ r(u,y)} \lor \lnot p(x,z) }}}$$

$$\forall y ~ \boxed{ \exists x \boxed{\exists z \boxed{ \exists u \boxed{ r(u,y) \lor \lnot p(x,z) }}}}\tag{D}$$

And it is in prenex form. (B) is equivalent to 3. (C) is equivalent to 4. (D) is equivalent to 5.

And occasionally shortcuts can be used to make the resulting prenex not so large:

$$\forall x ~ A(x) \land \forall y ~ B(y) = \forall z~A(z) \land B(z)$$ $$\exists x ~ A(x) \lor \exists y ~ B(y) = \exists z~A(z) \lor B(z)$$

A shortcut could have been used on step (T) to combine $z$ and $u$ into a single quantifier $w$:

$$\forall y ~ \boxed{ \exists x \boxed{ \boxed{\exists z ~\lnot p(x,z)} \lor \boxed{\exists u~ r(u,y)} }} \tag{T}$$

$$\forall y ~ \boxed{ \exists x \boxed{ \exists w \boxed{\lnot p(x,w) \lor r(w,y)} }} $$

And that is a much simpler prenex form. Hopefully your book makes it clear that a single expression can have multiple prenex forms, as above.