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.

For example:

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

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

*uniqueness quantifier*, or

*unique existential quantifier*. It is usually read "there exists one and only one", or "there exists an 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*)

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

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

*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*).

*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*