Existential quantifier

An existential quantifier is the symbol ∃ in predicate calculus. It roughly represents the phrase "for some" or "there exists". For example

∃ x (x²=25)

means "there exists an x such that x²=25".

The unique existential quantifer is the symbol ∃!. For example,

∃! x (x-2) = 4

means "there exists an unique x such that x-2 = 4".

History of the Quantifer

TODO

See Existential quantification for details.