# Uniqueness quantification

In predicate logic and technical fields that depend on it, **uniqueness quantification**, or **unique existential quantification**, is an attempt to formalise the notion of something being true for *exactly one* thing, or exactly one thing of a certain type.

Uniqueness quantification is a kind of quantification; more information about quantification in general is in the Quantification article. This article deals with the ideas peculiar to uniqueness quantification. A generalization of uniqueness quantification is counting quantification.

For example:

- There is exactly one natural number
*x*such that*x*- 2 = 4.

Symbolically, this can be written:

- ∃!
*x*in**N**,*x*- 2 = 4

The symbol "∃!" is called the *uniqueness quantifier*, or *unique existential quantifier*. It is usually read "there exists one and only one", or "there exists a unique"
(Several variations on the grammar for this symbol exist, as well as for how it's read.)

Uniqueness quantification is usually thought of as a combination of universal quantification ("for all", "∀"), existential quantification ("for some", "∃"), and equality ("equals", "=").
Thus if *P*(*x*) is the predicate being quantified over (in our example above, *P*(*x*) is "*x* - 2 = 4"), then ∃!*x*, *P*(*x*) means:

- (∃
*a*,*P*(*a*) ∧ (∀*b*,*P*(*b*) → (*a*=*b*)))

In words:

- For some
*a*,*P*(*a*) and for all*b*, if*P*(*b*), then*a*equals*b*.

Or even more succinctly:

- For some
*a*such that*P*(*a*), for all*b*such that*P*(*b*),*a*equals*b*.

Here, *a* is the unique object such that *P*(*a*); it exists, and furthermore, if any other object *b* also satisfies *P*(*b*), then *b* must be that same unique object *a*.

The statement that exactly one *x* exists such that *P*(*x*) can also be seen as a logical conjunction of two weaker statements:

- For
*at least*one*x*,*P*(*x*); and - For
*at most*one*x*,*P*(*x*).

The 1st of these is simply existential quantification; ∃*x*, *P*(*x*).
The 2nd is uniqueness *without* existence, sometimes written !*x*, *P*(*x*).
This is defined as:

- ∀
*a*, ∀*b*,*P*(*a*) ∧*P*(*b*) →*a*=*b*

The conjunction of these statements is logically equivalent to the single statement given earlier. But in practice, proving unique existence is often done by proving these two separate statements.

**See also:** one and only one.nl:Uniciteit
sv:Unik