Does the unique existential quantifier commute with the existential quantifier?

Given some function involving two variables, $\mathit p(x,y)$, is the formula $$\mathit \exists!x\exists yp(x,y)$$ equivalent to $$\mathit\exists y\exists!xp(x,y)$$ I have tried writing out the formal definition for the unique existential quantifier, but I get stuck simplifying the statement when the unique quantifier is first. I have also tried giving $\mathit p(x,y)$ some meaning and talking through it, but I can't decide if they mean the same thing. Any help is appreciated!

Solution 1:

No, they do not commute.

Consider for example the nonnegative reals as a linear order. Then $$\exists x\exists !y(y\le x)$$ is true (take $x=0$), but $$\exists!y \exists x(y\le x)$$ is false since for every $y$ there is some $x$ with $y\le x$.

This becomes less surprising when we "unpack" $\exists!$. There are a few ways to do this, but I think the simplest is to view "$\exists !x\varphi(x,...)$" as an abbreviation for "$\exists x\forall z(\varphi(z,...)\leftrightarrow x=z)$." Then we have:

• "$\exists x\exists!y\varphi(x,y)$" is an abbreviation for $$\exists x\exists y\forall z(\varphi(x,z)\leftrightarrow y=z),$$

• while "$\exists!y\exists x\varphi(x,y)$" is an abbreviation for $$\exists y\forall z[(\exists x\varphi(x,z))\leftrightarrow y=z].$$

This has a clear instance of swapping $\forall$ and $\exists$ (in fact, it's even messier than that - unpack "$\leftrightarrow$" ...), so we should expect them to be inequivalent in general.

(There are of course other ways to unpack "$\exists!$," but they'll all yield the same general picture: despite the symbol suggesting only existentiality, it's hiding a very important universal quantifier, and so the usual dangers of $\forall/\exists$-switching carry over to $\exists!/\exists$-switching.)