Encyclopedia > There is

Article Content

Existential quantification

Redirected from There is

In predicate logic and technical fields that depend on it, existential quantification is an attempt to formalise the notion of something being true for at least one thing, or at least one thing of a certain type. Thus, it is a way of indicating in a finitary[?] way something about a perhaps infinite number of statements (specificially, that at least one is true); but the statements must all be expressible with a common template.

For example, suppose you wish to say

0² = 25, or 1² = 25, or 2² = 25, or so on.

This would seem to be a logical disjunction because of the repeated use of "or". But the "or so on" can't be interpreted as a disjunction in a formally logical fashion. Instead, rephrase the statement as

For some natural number x, x² = 25.

This is a single statement using existential quantification. Notice that this statement is really more precise than the original one. It may seem obvious that the phrase "or 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 existential quantification, on the other hand, the natural numbers are mentioned explicitly.

This particular example is true, because 5 is a natural number, and when we put 5 in for x, we get 5² = 25, which is true. In contrast, "For some natural number x, x² = 2" is false, because 2 is not a perfect square. However, "For some real number x, x² = 2" is true, because we could put √2, the principal square root of 2, in for x. We could also put in -√2 for x in this last case; it's no problem that there is more than one solution.

The form of an existential quantification

Every existential quantification statement uses a dummy variable[?], such as the x in the above example. x could be replaced with any other symbol, and the meaning of the statement wouldn't change, as long as that symbol isn't being used anywhere else. (In a less formal context, we might use a pronoun instead; for example, we could say "For some natural number, its square is equal to 25"; here, "it" takes the place of the dummy variable. Even less formally, "Some natural number has a square equal to 25".)

It's also necessary to specify the universe of discourse of the dummy variable. This allows us to capture the difference between, for example, "Something is evil" ("For some x, x is evil") and "Some human is evil" ("For some human x, x is evil"). In our example, the universe of discourse was originally the set of natural numbers; later we changed it to the set of real numbers. It's not necessary for the universe of discourse to be a set in terms of formal set theory, and existential quantification can be used in logical theories that don't make any reference to sets. Indeed, ordinary predicate logic usually takes the universe of discourse to be everything under discussion, at least at the fundamental level.

We said that the statements to be covered by an existential quantification must fit a certain template. Call this template P(x). That is, P(x) is a specific statement about x; formally, it should be a predicate in one variable. In the original example above, P(x) is the statement "x² = 25". P(x) is known as the (I don't know what it's called; can anybody help out here?). By the way, it's possible that P(x) doesn't mention x at all. You could take P(x) to be "The sky is blue" and say "For some natural number x, the sky is blue". This is usually a silly thing to say, since there's no reason to mention x in that case; you could just say "The sky is blue" and be done with it. Nevertheless, such a case may come up in a degenerate situation.

Several phrasings are used for existential quantification, such as:

There is something x such that x is P.
For some x, P(x).
There exists an x such that P(x).
For at least one x, P(x).

Symbolically, the statement can be written in different ways:

(∃x) P'x
∃x P'x
∃x, P(x)
∃x: P(x)
∃_x P(x)

(The last three symbolizations are uncommon nowadays.)

Informally, the "for some x" or "∃x" might well appear after P(x), or even in the middle of it if it's a long phrase. Formally, however, the phrase that introduces the dummy variable should always be placed in front. (In this example, the universe of discourse is everything under discussion, the most fundamental universe of discourse.)

The universe of discourse

How you restrict the universe of discourse depends on the nature of the underlying logical theory.

First, you might be using a theory with more than one type. For example, suppose that you're studying a formal set theory with ur-elements[?] (objects that are not sets), rather than ordinary set theory (where everything is a set). Then you could have two types of objects, sets and ur-elements, which might be indicated differently in your notation. For example, suppose that ur-elements are given by lowercase letters, while sets are given by uppercase letters. Then the statement

∃x, x is in A

says that the set A has at least one ur-element for a member, while the statement

∃X, X is in A

says that A has at least one set for a member. Either statement is weaker than the claim that A has some member at all. These statements can be read aloud as "For some ur-element x, ..." and "For some set X, ...", since "x" and "X" are difficult or impossible to distinguish by sound.

If you're using set theory (as almost all of mathematics does), then you can use sets themselves to define the universe of discourse. For example, if N is the set of natural numbers, then

∃x∈N, x² = 25

is a purely symbolic way of writing the example that began this article. This can be read as "For some x in N, ..." or "There exists an x in N such that ...".

Additionally, you can use logical conjunction to further restrict a universe of discourse to only those x such that some statement Q(x) is true. The statement

∃x, Q(x) ∧ P(x)

literally says

For some x, Q(x) and P(x).

but this is equivalent to

For some x such that Q(x), P(x).

Thus the universe of discourse has been restricted, in effect.

This can be used to cover both of the cases above. For example, to deal with ur-elements in untyped predicate logic (the ordinary kind), you just need a logical predicate[?] that says whether something is a set or an ur-element; say, Sx iff x is a set. Then to say that A has at least one member that is an ur-element, write

∃x, ¬Sx ∧ x is in A

Or, to say that some natural number has a square equal to 25, write

∃x, x ∈ N ∧ x² = 25

Indeed, these formulations may be used as definitions in an interpretation of typed logic in terms of untyped logic, or in a formalisation of set theory.

Properties

We need a list of algebraic properties of existential quantification, such as distributivity over disjunction, and so on.