Universal quantification

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

For example, suppose you wish to say

0 = 0, and 1 = 1, and 2 = 2, and so on.

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

For any natural number x, x = x.

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

This particular example is true, because you could put any natural number in for x and the statement "x = x" would be true. On the other hand, "For any natural number x, x = 2" is false, because you could put, say, 3 in for x and get the false statement "3 = 2". However, "For any even prime number x, x = 2" is true, because 2 is the only even prime number.

The form of a universal quantification

Every universal 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 any natural number, it is equal to itself"; here, "it" takes the place of the dummy variable. Even less formally, "Any natural number is equal to itself".)

It's also necessary to specify the universe of discourse of the dummy variable. This allows us to capture the difference between, for example, "Everything is evil" ("For any x, x is evil") and "All humans are evil" ("For any 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 even prime numbers. It's not necessary for the universe of discourse to be a set in terms of formal set theory, and universal 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 a universal 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 example above, P(x) is the statement "x = x". 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 any 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 universal quantification, such as:

For any x, P(x).
For all x, P(x).
For each x, P(x).
For every x, P(x).

Symbolically, the statement can be written in various ways:

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

(The last five symbolizations are uncommon nowadays.)

Informally, the "for any 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 of x 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 not in A

says that the set A has no ur-elements for members, while the statement

∀X, X is not in A

says that A has no sets for members. Only after making both statements can we conclude that A has no members at all. These statements can be read aloud as "For any ur-element x, ..." and "For any 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 scope. For example, if N is the set of natural numbers, then

∀x∈N, x = x

is a purely symbolic way of writing the example that began this article. This can be read as "For any x in N, ...".

Additionally, you can use material implication 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 any x, if Q(x), then P(x).

but this is equivalent to

For any 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 no members that are ur-elements, write

∀x, ¬Sx → x is not in A

Or, to say that any natural number is equal to itself, write

∀x, x ∈ N → x = x

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 universal quantification, such as distributivity over conjunction, and so on.