Equivalence of Definitions of Unique Existential Quantifier
Theorem
The following definitions of the concept of Unique Existential Quantifier are equivalent:
Definition 1
There exists a unique object $x$ such that $\map P x$, denoted $\exists ! x: \map P x$, if and only if:
- $\exists x : \paren {\map P x \land \forall y : \paren {\map P y \implies x = y} }$
In natural language, this means:
- There exists exactly one $x$ with the property $P$
- is logically equivalent to:
Definition 2
There exists a unique object $x$ such that $\map P x$, denoted $\exists ! x: \map P x$, if and only if:
- $\exists x : \forall y : \paren {\map P y \iff x = y}$
Definition 3
There exists a unique object $x$ such that $\map P x$, denoted $\exists ! x: \map P x$, if and only if both:
- $\exists x : \map P x$
and:
- $\forall y : \forall z : \paren {\paren {\map P y \land \map P z} \implies y = z }$
Proof
Definition 1 iff Definition 2
Suppose Definition 1, that for some $x$, both:
- $(1): \quad \map P x$
and:
- $(2): \quad \forall y : \paren {\map P y \implies x = y}$
From $(1)$:
- $x = y \implies \map P y$
From this and $(2)$, we conclude:
- $\exists x : \forall y : \paren {\map P y \iff x = y}$
Suppose Definition 2, that for some $x$ and every $y$:
- $\map P y \iff x = y$
Taking $y = x$ yields:
- $x = x \implies \map P x$
implying that $\map P x$.
Thus we conclude:
- $\exists x : \paren {\map P x \land \forall y : \paren {\map P y \implies x = y} }$
$\Box$
Definition 2 iff Definition 3
Suppose Definition 2, that for some $x$:
- $(1): \quad \forall y : \paren {\map P y \iff x = y}$
Taking $y = x$ yields:
- $x = x \implies \map P x$
implying that $\exists x : \map P x$.
Suppose $\map P y$ and $\map P z$ for arbitrary $y$ and $z$.
Then from $(1)$, $y = x$ and $z = x$, giving:
- $\forall y : \forall z : \paren {\paren {\map P y \land \map P z} \implies y = z}$
Suppose Definition 3, that:
- $(1): \quad \exists x : \map P x$
and for arbitrary $y$ and $z$:
- $(2): \quad \paren { \map P y \land \map P z } \implies y = z$
From $(2)$, take $z = x$:
- $\paren {\map P y \land \map P x} \implies y = x$
Thus, by $(1)$:
- $\map P y \implies x = y$
Suppose $x = y$.
From $(1)$, $\map P x$, yielding:
- $x = y \implies \map P y$
Thus:
- $\exists x : \forall y : \paren {\map P y \iff x = y}$
$\Box$
Definition 1 iff Definition 3
Suppose Definition 1, that for some $x$:
- $(1): \quad \map P x$
and:
- $(2): \quad \forall y : \paren {\map P y \implies x = y}$
Suppose that $\map P y$ and $\map P z$ for arbitrary $y$ and $z$.
From $(2)$, there is an $x$ such that $x = y$ and $x = z$.
Thus, for arbitrary $y$ and $z$:
- $\paren {\map P y \land \map P z} \implies y = z$
and from $(1)$:
- $\exists x : \map P x$
Suppose Definition 3, that there is an $x$ such that:
- $(1): \quad \map P x$
and that for arbitrary $y$ and $z$:
- $(2): \quad \paren {\map P y \land \map P z} \implies y = z$
Taking $z = x$, we have from $(2)$:
- $\paren {\map P y \land \map P x} \implies y = x$
Thus, from $\map P x$ in $(1)$:
- $\forall y : \paren {\map P y \implies x = y}$
Thus:
- $\exists x : \paren {\map P x \land \forall y : \paren {\map P y \implies x = y} }$
$\Box$