Existential quantification

Existential quantification

Type	Quantifier
Field	Mathematical logic
Statement	${\displaystyle \exists xP(x)}$ is true when ${\displaystyle P(x)}$ is true for at least one value of ${\displaystyle x}$.
Symbolic statement	${\displaystyle \exists xP(x)}$

In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, when used together with a predicate variable, is called an existential quantifier ("∃x" or "∃(x)" or "(∃x)"^[1]). Existential quantification is distinct from universal quantification ("for all"), which asserts that the property or relation holds for all members of the domain.^[2][3] Some sources use the term existentialization to refer to existential quantification.^[4]

Quantification in general is covered in the article on quantification (logic). The existential quantifier is encoded as U+2203 ∃ THERE EXISTS in Unicode, and as \exists in LaTeX and related formula editors.