I know that prenex normal form (PNF) is not canonical, and there is an example in Wikipedia showing two equivalent formulae in PNF that differ in their prefixes, but have equal matrices:
$\forall x \forall z((\phi \lor \psi) \to \rho)$
$\forall z \forall x((\phi \lor \psi) \to \rho)$
By "canonical", I am following this definition: "a canonical form specifies a unique representation for every object, while a normal form simply specifies its form, without the requirement of uniqueness."
The "uniqueness" is also ambiguous, so I will explain what I mean by two formulae in Sum of Products (SoP) to be the "same". For instance, SoP is canonical because every two equivalent formulae in SoP will have the "same" minterms. Here, I am assuming that (i) the order of the conjunctions within minterns does not affect their "syntactic sameness", and (ii) the order of the minterms within formulae in SoP normal form does not affect their "syntactic sameness".
This is not true for disjunctive normal form (DNF), as the following formulae are equivalent and are both in DNF, but are not the "same", in the sense of having the "same" product terms, where (i) the order of the conjunctions within product terms does not affect their "syntactic sameness", and (ii) the order of the product terms within formulae in DNF does not affect their "syntactic sameness".
$\varphi\hphantom{'} \triangleq (a \land \neg b) \lor (b \land \neg c) \lor (\neg a \land c)$
$\varphi' \triangleq (\neg a \land b) \lor (\neg b \land c) \lor (a \land \neg c)$
Having said that, I would like to know if, when transforming a first-order formula to PNF and then to a first-order version of the SoP normal form, which is canonical for propositional logic (e.g., by interpreting predications in the matrix of the prenex form as propositions), will the composite transformation—name it PSoP—be canonical? In other words, given two first-order formulae $\varphi$ and $\varphi'$ in PSoP and such that $\varphi \equiv \varphi'$, do $\varphi$ and $\varphi'$ only differ on the variables, so one could transform $\varphi$ into $\varphi'$ by a renaming substitution?
P.S.: This question relates to https://math.stackexchange.com/questions/1095510/would-a-prenex-blake-normal-form-be-canonical