What is dual to "There exists unique?"
Solution 1:
I suppose you could define $\forall!$ by $$\forall!x \psi(x) \leftrightarrow \forall x[\psi(x) \vee \exists y(\neg \psi(y) \wedge y \ne x)]$$ ("Either $\psi$ holds here or it fails somewhere else too" / "Either $\psi$ is true everywhere or there are at least two counterexamples")
Then $\exists ! = \neg \forall ! \neg$ and $\forall ! = \neg \exists ! \neg$ in the same sense that $\exists = \neg \forall \neg$ and so on: really $\exists = \neg \forall \neg$ is just shorthand for $\exists x \phi(x) \leftrightarrow \neg \forall x \neg \phi(x)$.
Why? Well, $\exists ! x\ \phi(x)$ is shorthand for $$\exists x [\phi(x) \wedge \forall y (\phi(y) \to y=x)]$$ Dualising the quantifiers gives $$\neg \forall x \neg [\phi(x) \wedge \neg \exists y\neg(\phi(y) \to y=x)]$$ which is equivalent to $$\neg\forall x[\neg \phi(x) \vee \exists y (\phi(y) \wedge y \ne x)]$$ So we have $$\exists ! x \phi(x) \leftrightarrow \neg \forall ! x \neg \phi(x)$$ And so on.
Solution 2:
This answer doesn't really differ from Clive Newstead's answer, but arrives at essentially the same place via a slightly different approach.
Note that
- $( \exists x ) ( \phi (x) )$ holds iff $\{ x : \phi (x) \} \neq \varnothing$;
- $( \forall x ) ( \phi (x) )$ holds iff $\{ x : \neg \phi (x) \} = \varnothing$.
Another set of dual quantifiers are $\exists^\infty$ and $\forall^\infty$ which satisfy
- $( \exists^\infty x ) ( \phi (x) )$ holds iff $\{ x : \phi (x) \}$ is infinite (i.e., is not finite);
- $( \forall^\infty x ) ( \phi (x) )$ holds iff $\{ x : \neg \phi (x) \}$ is finite.
So by analogy, since,
- $( \exists ! x )( \phi (x) )$ holds iff $| \{ x : \phi (x) \} | = 1$
this would imply that the natural definition of $\forall !$ would be
- $ ( \forall ! x ) ( \phi (x) )$ holds iff $| \{ x : \neg \phi (x) \} | \neq 1$.
Solution 3:
If you have a formula $\phi$ for which you proved that $\exists ! x, \phi(x)$ (i.e. $\exists x, \phi(x) \land \forall y, \phi(y) \implies y=x$), then you have :
$(\exists x. \phi(x) \land \psi(x)) \iff (\forall x. \phi(x) \implies \psi(x))$, and so the connective $\exists x.\phi(x) \land \cdot$ is equivalent to its dual $\forall x. \phi(x) \implies \cdot$
So the "let $x$ be the unique object satisfying $\phi$ in ..." connective (you could write it $\nabla_\phi x. \psi(x)$) is self-dual, and behaves rather "neutrally". For example it "commutes" with almost everything : you can push it inside of or pull it out of formulas easily (as long as you don't break $\phi$ by pulling out of quantifiers over variables appearing in $\phi$)