Editing Uniqueness quantification (section)

== Generalizations ==
The uniqueness quantification can be generalized into [[counting quantification]] (or numerical quantification<ref>{{Cite web|url=http://persweb.wabash.edu/facstaff/helmang/phi270-1314F/phi270PDF/phi270text/phi270txt8/phi270txt83/phi270txt83(4up).pdf|title=Numerical quantification|last=Helman|first=Glen|date=August 1, 2013|website=persweb.wabash.edu|access-date=2019-12-14}}</ref>). This includes both quantification of the form "exactly ''k'' objects exist such that …" as well as "infinitely many objects exist such that …" and "only finitely many objects exist such that…". The first of these forms is expressible using ordinary quantifiers, but the latter two cannot be expressed in ordinary [[first-order logic]].<ref>This is a consequence of the [[compactness theorem]].</ref>

Uniqueness depends on a notion of [[equality (mathematics)|equality]]. Loosening this to a coarser [[equivalence relation]] yields quantification of uniqueness [[up to]] that equivalence (under this framework, regular uniqueness is "uniqueness up to equality"). This is called [[essentially unique]]. For example, many concepts in [[category theory]] are defined to be unique up to [[isomorphism]].

The exclamation mark <math>!</math> can be also used as a separate quantification symbol, so <math>(\exists ! x. P(x))\leftrightarrow ((\exists x. P(x))\land (! x. P(x)))</math>, where <math>(! x. P(x)) := (\forall a \forall b. P(a)\land P(b)\rightarrow a=b)</math>. E.g. it can be safely used in the [[replacement axiom]], instead of <math>\exists !</math>.