I find the sign of equality beautiful.

So, 3 = 1 + 1 + 1? Or can more be done to simplify the symbolism?

Is the latter quote from Quine metaphysical in your view?

Perhaps Quine doesn't consider your rules rules of passage per se in that what you end up with isn't an equivalence with a (possibly different) quantifier that has passed inside--it's not a simple rule that just involves merely "passing" the quantifier inside and then maybe changing the quantifier (while leaving the logical operator alone). It is a very well-known theorem that every first-order formula (even equivalences) is equivalent to one in prenex normal form; as for the reverse direction, well, I have seen less arguments needing to go that direction. I must admit your rule (2)

though right is not something I recall seeing or thinking about before; it is interesting enough that perhaps it should be taught more. If one were interested in a formula with no quantifier binding more than one instance of a variable, and wanted to get an equivalent formula with all the quantifiers pushed in next to the function symbol involving that variable, your rules would be useful, showing the method would work even with formulas involving equivalences.

Let "<" denote "entails" (or implication if you don't know the difference), "\x/" denote "exists an x" and "/x\" denote "for all x". An interesting observation about the prenex rules (the phrase "rules of passage" annoys me) for implication concerns B -> \x/ C < \x/ (B -> C) and /x\ B -> C < \x/(B -> C). Breaking the implication prenex rules into their eight separate parts, these two parts are the only difficult ones to prove (assuming reasonable axioms of logic chosen to make the axioms of logic analogous to the natural ones of a lattice), requiring one to consider exactly what truth values there are, and yet they are the only parts that hold regardless of what formulas are substituted for B and C--no need to worry in these two parts about what variables are free where, etc.

Since the forward part of your rule (2) is trivial, what you did that was interesting (the backwards direction of your rule (2)) was to combine the two interesting parts of the prenex rules for implication into one rule; but maybe it isn't so great after all since unlike the two interesting parts, it really needs p to not involve x. E.g., if Fx is x = 0, then changing p to ~ x = 0 makes rule fail.

I think these rules for equivalence should be added to the list just to complete the list of rules of passage.

All of these theorems assume that p has no free x.

We cannot substitute ~x = 0 for p.