Definition:Universal Quantifier

From ProofWiki
Jump to navigation Jump to search

Definition

The symbol $\forall$ is called the universal quantifier.

It expresses the fact that, in a particular universe of discourse, all objects have a particular property.


That is:

$\forall x:$

means:

For all objects $x$, it is true that ...


In the language of set theory, this can be formally defined:

$\forall x \in S: \map P x := \set {x \in S: \map P x} = S$

where $S$ is some set and $\map P x$ is a propositional function on $S$.


Propositional Expansion

The universal quantifier can be considered as a repeated conjunction:

Suppose our universe of discourse consists of the objects $\mathbf X_1, \mathbf X_2, \mathbf X_3, \ldots$ and so on.

Let $\forall$ be the universal quantifier.

What $\forall x: \map P x$ means is:

$\mathbf X_1$ has property $P$, and $\mathbf X_2$ has property $P$, and $\mathbf X_3$ has property $P$, and ...

This translates into propositional logic as:

$\map P {\mathbf X_1} \land \map P {\mathbf X_2} \land \map P {\mathbf X_3} \land \ldots$


This expression of $\forall x$ as a conjunction is known as the propositional expansion of $\forall x$.


The propositional expansion for the universal quantifier can exist in actuality only when the number of objects in the universe is finite.

If the universe is infinite, then the propositional expansion can exist only conceptually, and the universal quantifier cannot be eliminated.


Also see

  • Results about the Universal Quantifier can be found here.


Notational Variants

Various symbols are encountered that denote the concept of universal quantifier:

Symbol Origin
$\forall x$ Gerhard Gentzen: Untersuchungen über das logische Schließen (1935)
$\left({x}\right)$ 1910: Alfred North Whitehead and Bertrand Russell: Principia Mathematica
$\Pi x$ Łukasiewicz's Polish notation
$\wedge x$ or $\bigwedge x$
$\displaystyle \operatorname{\Large {\textsf A} } \limits_{x, y, \dotsc}$ 1946: Alfred Tarski: Introduction to Logic and to the Methodology of Deductive Sciences


Historical Note

The symbol $\forall$ for the universal quantifier was first used by Gerhard Karl Erich Gentzen in 1935: Untersuchungen über das logische Schließen. II (Math. Z. Vol. 39 (3): 405 – 431).

He invented it in analogy with the existential quantifier symbol $\exists$ which he borrowed from Bertrand Russell.

Russell himself used the notation $\paren x$ for for all $x$. See his 1908: Mathematical Logic as Based on the Theory of Types (Amer. J. Math. Vol. 30: 222 – 262).


Sources