Order of quantifiers in prenex normal form I was wondering while doing some transformation into prenex form whether there is a situation when it does matter in what order you pull out the quantifiers to the front. If you know a good example, could you please share it? Thanks!

In converting a wff $\varphi$ by stages into an equivalent wff in some normal form, at each step we go from a wff to something equivalent.

So whatever order we apply steps in, if there is a choice in your normalization procedure, then starting with $\varphi$ we must end up with something still equivalent to the original $\varphi$.

So in _that_ sense, at any rate, it can't matter what order we apply steps in. It can't logically matter in what order you pull out the quantifiers or other logical apparatus to the front, when there is a choice. Outputs will be logically equivalent.