In predicate logic '''existential quantification''' is an attempt to formalize the notion that something (a logical predicate) is true for ''something'' or at least one relevant thing
The resulting statement is an

**existentially quantified** statement and we have

**existentially quantified** over the predicateIn

symbolic logic the

**existential quantifier** (typically "∃") is the symbol used to denote existential quantification

Quantification in general is covered in the article

Quantification while this article discusses

existential quantification specifically

## Basics

Suppose you wish to write a

formula which is true if and only if some

natural number multiplied by itself is 25. A naive approach you might try is the following:

- 0·0 = 25,
**or** 1·1 = 25, **or** 2·2 = 25, **or** 3·3 = 25, and so on

This would seem to be a

logical disjunction because of the repeated use of "or"However the "and so on" makes this impossible to interpret as a disjunction in formal logicInstead we rephrase the statement as

- For some natural number
*n* *n*·*n* = 25

This is a single statement using existential quantification

Notice that this statement is really more precise than the original oneIt may seem obvious that the phrase "and so on" is meant to include all

natural numbers and nothing more but this wasn't explicitly stated which is essentially the

reason that the phrase couldn't be interpreted formally In the quantified statement on the

other hand the natural numbers are mentioned explicitly

This particular example is true because 5 is a

natural number and when we substitute 5 for

*n* we produce "5·5 = 25" which is trueIt does not matter that "

*n*·

*n* = 25" is false for

*most* natural numbers

*n* in

fact false for all of them

*except* 5; even the existence of a single

solution is enough to prove the

existential quantification true(Of course multiple solutions can only help!)In contrast "For some even number

*n* *n*·

*n* = 25" is false because there are no even solutions

On the

other hand "For some odd number

*n* *n*·

*n* = 25" is true because the

solution 5 is oddThis demonstrates the importance of the

*domain of discourse* which specifies which values the variable

*n* is allowed to takeFurther information on using domains of

discourse with quantified statements can be found in the

Quantification articleBut in particular note that if you wish to restrict the domain of

discourse to consist only of those objects that satisfy a certain predicate then for

existential quantification you do this with a

logical conjunctionFor example "For some odd

number *n* *n*·

*n* = 25" is logically equivalent to "For some

natural number *n* *n* is odd and

*n*·

*n* = 25"Here the "and"

construction indicates the logical conjunction

In

symbolic logic we use the existential quantifier "∃" (a backwards letter "E" in a sans-serif font) to indicate existential quantificationThus if

*P*(

*a* *b* *c*) is the predicate "

*a*·

*b* = c" and

**N** is the set of natural numbers then

- $exists\{n\}\{in\}mathbf\{N\}\; P(nn25)$

is the (true) statement

- For some natural number
*n* *n*·*n* = 25

Similarly if

*Q*(

*n*) is the predicate "

*n* is even" then

- $exists\{n\}\{in\}mathbf\{N\}\; big(Q(n);!;!\; \{wedge\};!;!\; P(nn25)big)$

is the (false) statement

- For some even number
*n* *n*·*n* = 25

Several variations in the notation for

quantification (which apply to all forms) can be found in the

Quantification article

## Properties

*We need a list of algebraic properties of existential quantification such as distributivity over disjunction and so on. Also rules of inference*