Existential quantification

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)"). Existential quantification is distinct from universal quantification ("for all"), which asserts that the property or relation holds for all members of the domain. Some sources use the term existentialization to refer to existential quantification. Consider a formula that states that some natural number multiplied by itself is 25. 0·0 = 25, or 1·1 = 25, or 2·2 = 25, or 3·3 = 25, ... This would seem to be a logical disjunction because of the repeated use of "or". However, the ellipses make this impossible to integrate and to interpret it as a disjunction in formal logic. Instead, the statement could be rephrased more formally as For some natural number n, n·n = 25. This is a single statement using existential quantification. This statement is more precise than the original one, since the phrase "and so on" does not necessarily include all natural numbers and exclude everything else. And since the domain was not stated explicitly, the phrase could not be interpreted formally. In the quantified statement, however, 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 true. It does not matter that "n·n = 25" is only true for a single natural number, 5; even the existence of a single solution is enough to prove this existential quantification as being true. In contrast, "For some even number n, n·n = 25" is false, because there are no even solutions. The domain of discourse, which specifies the values the variable n is allowed to take, is therefore critical to a statement's trueness or falseness. Logical conjunctions are used to restrict the domain of discourse to fulfill a given predicate.