Editing Uniqueness quantification (section)

== Reduction to ordinary existential and universal quantification ==
Uniqueness quantification can be expressed in terms of the [[existential quantifier|existential]] and [[universal quantifier|universal]] quantifiers of [[predicate logic]], by defining the formula <math>\exists ! x P(x)</math> to mean<ref>{{Cite book |last=Kleene |first=Stephen Cole |author-link=Stephen Cole Kleene |url=https://archive.org/details/mathematicallogi0000klee/page/154 |title=Mathematical logic |date=1967 |publisher=Wiley |isbn=978-0-471-49033-3 |location=New York |pages=154 |lccn=66-26747}}</ref>

:<math>\exists x\,( P(x) \, \wedge \neg \exists y\,(P(y) \wedge y  \ne x)),</math>
which is logically equivalent to
:<math>\exists x \, ( P(x) \wedge \forall y\,(P(y) \to y = x)).</math>

An equivalent definition that separates the notions of existence and uniqueness into two clauses, at the expense of brevity, is
:<math>\exists x\, P(x) \wedge \forall y\, \forall z\,[(P(y) \wedge P(z)) \to y = z].</math>

Another equivalent definition, which has the advantage of brevity, is
:<math>\exists x\,\forall y\,(P(y) \leftrightarrow y = x).</math>