Existential quantifier: notation, semantics, and logical rules

Notation and simple example

A common way to write an existential statement is , which declares that some natural number equals 3+5. More generally, one writes expressions of the form , where the predicate is a property or relation on elements of the domain. Such a formula is true exactly when at least one value of the variable x in the domain makes P(x) true.

Formal meaning

• Domain: Truth of an existential formula depends on the chosen domain (the universe of discourse). If the domain is empty, an existential claim is false.
• Truth condition: The sentence ∃x P(x) is true iff there exists an element a in the domain such that P(a) holds.
• Binding and scope: The quantifier binds occurrences of the variable that fall within its scope; variables outside that scope remain free.

Relationship to other logical operators

The existence quantifier contrasts with the universal quantifier, which asserts that a property holds for every element of the domain. There are standard equivalences involving negation and the two quantifiers: for any predicate P, the negation of an existential statement is equivalent to a universal statement about the negation of P (formally, ¬∃x P(x) is equivalent to ∀x ¬P(x)), and similarly ¬∀x P(x) is equivalent to ∃x ¬P(x). These equivalences are part of basic first-order logic and are used frequently in proofs.

Usage notes

1. When proving an existential claim, it suffices to exhibit a concrete example or construct an element that satisfies the predicate.
2. In formal derivations, existential instantiation (introducing a fresh name for a witness) and existential generalization (deriving an existential statement from a specific example) are standard rules of inference.
3. Care must be taken with the domain: restricting the domain (for example, writing ∃x∈S P(x)) is syntactic sugar for introducing a predicate that tests membership in S together with P(x).

See also the article on quantifier for broader discussion of quantifiers in logic and their formal properties.