Help with prenex normal form

LEQV = Logically equivalent

I need help changing

∀xA(x) ^ ∀xB(x) ^ ∀xC(x) → ∀xD(x)

into PNF (such that the only connectives in the quantifier free portion have to be →)

∀xA(x) ^ ∀xB(x) ^ ∀xC(x) → ∀xD(x)

LEQV

￢ ( ∀xA(x) ^ ∀xB(x) ^ ∀xC(x) ) v ∀xD(x) [→ Law]

LEQV

( ∃x￢A(x) v ∃x￢B(x) v ∃x￢C(x) ) v ∀xD(x) [Duality of quantifiers law]

LEQV

∃x1∃x2∃x3∀x ( ( ￢A(x1) v ￢B(x2) v ￢C(x3) ) v D(x) ) [pulling quantifiers out]

LEQV

∃x1∃x2∃x3∀x ( ￢ ( A(x1) ^ B(x2) ^ C(x3) ) v D(x) ) [pulling￢ out]

LEQV

∃x1∃x2∃x3∀x ( ( A(x1) ^ B(x2) ^ C(x3) ) → D(x) ) [reverse → Law ]

I got here but I need the only connectives in the quantifier free portion to be →, right now the last step includes ^ symbols...

Thanks

Re: Help with prenex normal form

Re: Help with prenex normal form

Hmm is this right?

∀xA(x) ^ ∀xB(x) ^ ∀xC(x) → ∀xD(x)

LEQV

￢ ( ∀xA(x) ^ ∀xB(x) ^ ∀xC(x) ) v ∀xD(x) [→ Law]

LEQV

∃x￢A(x) v ∃x￢B(x) v ∃x￢C(x) v ∀xD(x) [Duality of quantifiers law]

LEQV

∃x1∃x2∃x3∀x ( ￢A(x1) v ￢B(x2) v ￢C(x3) v D(x) ) [pulling quantifiers out]

LEQV

∃x1∃x2∃x3∀x ( A(x1) → (￢B(x2) v ￢C(x3) v D(x) ) ) [reverse → Law ]

LEQV

∃x1∃x2∃x3∀x ( A(x1) →( B(x2) →( ￢C(x3) v D(x) )) ) [reverse → Law ]

LEQV

∃x1∃x2∃x3∀x ( A(x1) →( (B(x2) → (C(x3) → D(x) )) ) [reverse → Law ]

Re: Help with prenex normal form

→ v D(x)

is not syntactical.

I guess you mean:

Ax1-> (Bx2 -> (Cx3-> Dx))

Re: Help with prenex normal form

yeah, i edited the last post to fix it, but other than it, is each line logically equivilant?

Re: Help with prenex normal form

Darn, I messed up. I better doublecheck. I need to doublecheck the order of the quantifiers.

Re: Help with prenex normal form

Unless I'm missing something (and I'll use 'V' and 'E' as the quantifiers), we have:

(VyAy & VzBz & VwCw) -> VxDx

equivalent to

VxEyzw(Ay -> (Bz -> (Cw -> Dx)))

But I don't see how you would get

(VyAy & VzBz & VwCw) -> VxDx

equivalent to

EyzwVx(Ay -> (Bz -> (Cw -> Dx)))

I think I was correct when I said (before edits) that you reversed the correct order of quantifiers when you "pulled out".

Re: Help with prenex normal form

Now I am confused...

I thought I could do what I did in post#3, and since it ended up leqv to the last one, it has to be leqv.

Re: Help with prenex normal form

Look at your line where you pulled out the quantifiers. I think you incorrectly reversed the order.

Re: Help with prenex normal form

I don't see how this is wrong

∃x1∃x2∃x3∀x ( ￢A(x1) v ￢B(x2) v ￢C(x3) v D(x) ) [pulling quantifiers out]

because when I pull out the quantifiers, I renamed the variables using this law

Discrete Structures, Logic, and ... - Google Books

so each variable in the quantifiers are different, so the order shouldn't matter right?

Re: Help with prenex normal form

Suppose $\displaystyle \mathcal{Q}_1$ and $\displaystyle \mathcal{Q}_2$ are quantifiers (∀ or ∃) and $\displaystyle \star$ is ∧ or ∨. Then

$\displaystyle (\mathcal{Q}_1x\,A(x))\star(\mathcal{Q}_2y\,B(y))$

is equivalent to both

$\displaystyle \mathcal{Q}_1x\,\mathcal{Q}_2y\,(A(x)\star B(y))$

and

$\displaystyle \mathcal{Q}_2y\,\mathcal{Q}_1x\,(A(x)\star B(y))$

(assuming x does not occur freely in B and y does not occur freely in A). Therefore, in this problem the order of quantifiers in the prenex form does not matter.

Re: Help with prenex normal form

Re: Help with prenex normal form

Re: Help with prenex normal form

Yeah, my mistake. Both are correct.