Prenex normal form: moving quantifiers

Printable View

February 19th 2010, 07:27 AM
boon

Prenex normal form: moving quantifiers

Hi,

I'm trying to derive a Prenex normal form but I can't figure out in what order the quantifiers should be moved. I haven't been able to find a paper that would address this problem. Consider the following example:

AxP(x) v EyQ(y)

Doesn't seem difficult, but which quantifier should I move to the front first? I see it could go either this way:

Ax(P(x) v EyQ(y))
AxEy(P(x) v Q(y))

or this way:

Ey(AxP(x) v Q(y))
EyAx(P(x) v Q(y))

Perhaps the order doesn't matter in this example, I'm not sure, but I understand there are cases where it does matter. So what would be the correct way to handle these? Or does the order ever matter?

(E represents the existential quantifier, A represents the universal quantifier, and v is OR)

Edit: The conclusion I've reached is that the order doesn't matter as long as we have predicates with only one variable. As for multiple variables, I'd assume the quantifiers have to be in the order their variables appear in the predicates. Can anyone confirm this?
February 21st 2010, 02:14 PM
emakarov

Quote:

Edit: The conclusion I've reached is that the order doesn't matter as long as we have predicates with only one variable. As for multiple variables, I'd assume the quantifiers have to be in the order their variables appear in the predicates. Can anyone confirm this?

A formula $(\mathcal{Q}_1 P_1(x_1))\star(\mathcal{Q}_2 P_2(x_2))$ , where $\mathcal{Q}_i$ denote either $\forall$ or $\exists$ and $\star$ denotes either $\land$ or $\lor$ (but no implication!), is equivalent to both $\mathcal{Q}_1x_1\,\mathcal{Q}_2x_2.\, P_1(x_1)\star P_2(x_2)$ and $\mathcal{Q}_2x_2\,\mathcal{Q}_1x_1.\, P_1(x_1)\star P_2(x_2)$ . (I put a period after a quantified variable when the scope of the quantifier extends as far to the right as possible.)

Sometimes there are simpler prenex forms. $(\forall x_1 P_1(x_1))\land(\forall x_2 P_2(x_2))$ is equivalent to $\forall x.\,P_1(x)\land P_2(x)$ and, dually, $(\exists x_1 P_1(x_1))\lor(\exists x_2 P_2(x_2))$ is equivalent to $\exists x.\,P_1(x)\lor P_2(x)$ . This works because universal quantification is basically an infinite conjunction and the order of conjuncts does not matter.

In general, $\mathcal{Q}_1x_1\,\mathcal{Q}_2x_2.\, P(x_1,x_2)$ is equivalent to $\mathcal{Q}_2x_2\,\mathcal{Q}_1x_1.\, P(x_1,x_2)$ when $\mathcal{Q}_1$ and $\mathcal{Q}_2$ are either both universal or both existential. There is a huge difference between $\forall x_1\exists x_2\,P(x_1,x_2)$ and $\exists x_2\forall x_1\,P(x_1,x_2)$ . The important point here is the "interaction" of $x_1$ and $x_2$ .
February 23rd 2010, 08:01 AM
boon

Alright, thanks for the reply. I understand it now.