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.

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 scope 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 scope was the set of natural numbers. It's not necessary for the scope 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 scope 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. 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 degeneracy is allowed.

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 also be written in various ways, including:

∀x, P(x)
∀_x P(x)
(∀x) P(x)
(x) P(x)

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 scope of x is everything under discussion, the most fundamental scope.)

The scope

How you restrict the scope 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 set theory with ur-elements (objects that are not sets), rather than ordinary formal 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 ∉ A

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

∀X, X ∉ 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.

But if you're using set theory (as almost all of mathematics does), then you can use sets themselves to define scope. 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 scope 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 scope 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 ∉ 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.