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?