In predicate logic, universal quantification is an attempt to formalise the notion that something (a logical predicate) is true for everything, or every relevant thing. The resulting statement is a universally quantified statement, and we have universally quantified over the predicate. In symbolic logic, the universal quantifier (typically "∀") is the symbol used to denote universal quantification.

Quantification in general is covered in the article quantification, while this article discusses universal quantification specifically.

Basics

Suppose you wish to say

2·0 = 0 + 0, and 2·1 = 1 + 1, and 2·2 = 2 + 2, etc.

This would seem to be a logical conjunction because of the repeated use of "and". But the "etc" can't be interpreted as a conjunction in formal logic. Instead, rephrase the statement as

For any natural number n, 2·n = n + n.

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 "etc" 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 n and the statement "2·n = n + n" would be true. In contrast, "For any natural number n, 2·n > 2 + n" is false, because you replace n with, say, 1 and get the false statement "2·1 > 2 + 1". It doesn't matter that "2·n > 2 + n" is true for most natural numbers n; even the existence of a single counterexample is enough to prove the universal quantification false.

On the other hand, "For any composite number n, 2·n > 2 + n" is true, because none of the counterexamples are composite numbers. This indicates the importance of the domain of discourse, which specifies which values n is allowed to take. Further information on using domains of discourse with quantified statements can be found in the Quantification article. But 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 universal quantification, you do this with a logical conditional. For example, "For any composite number n, 2·n > 2 + n" is logically equivalent to "For any natural number n, if n is composite, then 2·n > 2 + n". Here the "if ... then" construction indicates the logical conditional.

In symbolic logic, we use the universal quantifier "∀" (an upside-down letter "A" in a sans-serif font) to indicate universal quantification. Thus if P(n) is the predicate "2·n > 2 + n" and N is the set of natural numbers, then

is the (false) statement

For any natural number n, 2·n > 2 + n.

Similarly, if Q(n) is the predicate "n is composite", then

is the (true) statement

For any composite number n, 2·n > 2 + n.

Several variations in the notation for quantification (which apply to all forms) can be found in the quantification article. But there is a special notation used only for universal quantification, which we also give here:

The parentheses indicate universal quantification by default.

Properties

We need a list of algebraic properties of universal quantification, such as distributivity over conjunction, and so on. Also rules of inference.

Discuss universally quantified types in type theory.