1. ## Prenex Normal Forms

Find a predicate form in prenex normal form which is logically equivalent to using the equivalences:

(a) $((Agxy \vee Bz) \to \exists y (By \to Bgy))$

(b) $(\forall x (Cxyz \to Bx) \wedge \neg \exists z \forall x (Dzy \to Dxy))$

Attempt:

(a) $((Agxy \vee Bz) \to \exists y (By \to Bgy))$

Here we only have one quantifier to be shifted to the front, so we can use equivalence number 12 to get

$\exists y ((Agxy \vee Bz) \to (By \to Bgy))$

Is this right? Because we are only justified in using this equivalence if the variable y doesn not occur free in $(Agxy \vee Bz)$, but we don't know that since y doesn't not appear in the scope of any quantifiers in it...

(b) $(\forall x(Cxyz \to Bx) \wedge \neg \exists z \forall x (Dzy \to Dxy))$

$\forall x ((Cxyz \to Bx) \wedge \neg \exists z \forall x (Dzy \to Dxy))$

In our case the variables are not distinct so we can't apply the equivalcences straight away, so we have to change bound variables first so that we can move quantifiers past the free variables:

$\forall x ((Cxyz \to Bx) \wedge \neg \exists z \forall w (Dzy \to Dwy))$

Now, I'm a bit confused about the negation, but I applied equivalence number 4

$\forall x \neg \exists z ((Cxyz \to Bx) \wedge \forall w (Dzy \to Dwy))$

Now we apply equivalence number 3

$\forall x \neg \exists z \forall w((Cxyz \to Bx) \wedge (Dzy \to Dwy))$

I would appreciate it if anyone could correct me.

2. ## Re: Prenex Normal Forms

Originally Posted by demode
(a) $((Agxy \vee Bz) \to \exists y (By \to Bgy))$

Here we only have one quantifier to be shifted to the front, so we can use equivalence number 12 to get

$\exists y ((Agxy \vee Bz) \to (By \to Bgy))$
You captured y in Agxy. The quantified y in the conclusion has to be renamed first.

Originally Posted by demode
(b) $(\forall x(Cxyz \to Bx) \wedge \neg \exists z \forall x (Dzy \to Dxy))$

$\forall x ((Cxyz \to Bx) \wedge \neg \exists z \forall x (Dzy \to Dxy))$

In our case the variables are not distinct so we can't apply the equivalcences straight away, so we have to change bound variables first so that we can move quantifiers past the free variables:

$\forall x ((Cxyz \to Bx) \wedge \neg \exists z \forall w (Dzy \to Dwy))$
But z also occurs free in the first part, so it has to be renamed as well.

Originally Posted by demode
Now, I'm a bit confused about the negation, but I applied equivalence number 4

$\forall x \neg \exists z ((Cxyz \to Bx) \wedge \forall w (Dzy \to Dwy))$
You need the equivalences $\neg\exists x\,A\Leftrightarrow\forall x\,\neg A$ and $\neg\forall x\,A\Leftrightarrow \exists x\,\neg A$.

3. ## Re: Prenex Normal Forms

Originally Posted by emakarov
But z also occurs free in the first part, so it has to be renamed as well.

You need the equivalences $\neg\exists x\,A\Leftrightarrow\forall x\,\neg A$ and $\neg\forall x\,A\Leftrightarrow \exists x\,\neg A$.
Is the following correct? I used the equivalence you mentioned:

$\forall x (( Cxyz \to Bx) \wedge \neg \exists z \forall w (Dzy \to Dwy))$

$\forall x (( Cxyz \to Bx) \wedge \neg \exists u \forall w (Duy \to Dwy))$

$\forall x (( Cxyz \to Bx) \wedge \forall u \forall w \neg(Duy \to Dwy))$

$\forall x \forall u \forall w(( Cxyz \to Bx) \wedge \neg(Duy \to Dwy))$

You captured y in Agxy. The quantified y in the conclusion has to be renamed first.
$((Agxy \vee Bz) \to \exists y (By \to Bgy))$

$((Agxy \vee Bz) \to \exists w (Bw \to Bgw))$

$\exists w ((Agxy \vee Bz) \to (Bw \to Bgw))$

Did I derive it correctly correct? It looks like it's in the prenex normal form since it's in the form $Q_1x_1Q_2x_2...Q_nx_n B$ (B being a predicate form with no quantifiers and $Q_n$ is any quantifier).

4. ## Re: Prenex Normal Forms

Originally Posted by demode
Is the following correct? I used the equivalence you mentioned:

$\forall x (( Cxyz \to Bx) \wedge \neg \exists z \forall w (Dzy \to Dwy))$

$\forall x (( Cxyz \to Bx) \wedge \neg \exists u \forall w (Duy \to Dwy))$

$\forall x (( Cxyz \to Bx) \wedge \forall u \forall w \neg(Duy \to Dwy))$

$\forall x \forall u \forall w(( Cxyz \to Bx) \wedge \neg(Duy \to Dwy))$
The quantifier of w should change from ∀ to ∃ when you carry negation over it. Otherwise, it seems correct.

Originally Posted by demode
$((Agxy \vee Bz) \to \exists y (By \to Bgy))$

$((Agxy \vee Bz) \to \exists w (Bw \to Bgw))$

$\exists w ((Agxy \vee Bz) \to (Bw \to Bgw))$

Did I derive it correctly correct?
Yes.

5. ## Re: Prenex Normal Forms

Originally Posted by emakarov
The quantifier of w should change from ∀ to ∃ when you carry negation over it. Otherwise, it seems correct.

Yes.
You mean every time I shift the negation to the right of the ∀ it changes to ∃ like this:

$\forall x (( Cxyz \to Bx) \wedge \neg \exists u \forall w (Duy \to Dwy))$

$\forall x (( Cxyz \to Bx) \wedge \forall u \exists w \neg(Duy \to Dwy))$

$\forall x \forall u \exists w(( Cxyz \to Bx) \wedge \neg(Duy \to Dwy))$

Is this okay now?

6. ## Re: Prenex Normal Forms

Originally Posted by demode
Is this okay now?
Yes.