In mathematical logic, quantifiers are formal counterparts of natural-language adjectives like all, some, most, few, etc. which indicate the number of objects satisfying a given property. More precisely, a quantifier is an operator that specifies how many individuals in the domain of discourse satisfy an open formula. For instance, the universal quantifier in the first-order formula expresses that all numbers in the domain are non-negative; this formula is true for the natural numbers domain, but false for the integer domain. On the other hand, the existential quantifier in the formula expresses that some numbers in the domain satisfy the given quadratic equation; indeed, both 2 and 3 do.
The most commonly used quantifiers are and . Other quantifiers are only definable within second-order logic or higher-order logics. Quantifiers have been generalized beginning with the work of Andrzej Mostowski and Per Lindström.
In a first-order logic statement, quantifications in the same type (either universal quantifications or existential quantifications) can be exchanged without changing the meaning of the statement. In contrast, the exchange of quantifications in different types changes the meaning. As an example for the latter, the only difference in the definition of uniform continuity and (ordinary) continuity is the order of quantifications.
Relations to logical conjunction and disjunction For a finite domain of discourse , the universally quantified formula is equivalent to the logical conjunction . Dually, the existentially quantified formula is equivalent to the logical disjunction . For example, if is the set of binary digits, the formula abbreviates , which evaluates to true.
Infinite domain of discourse
Consider the following statement (using dot notation for multiplication):
This has the appearance of an infinite conjunction of propositions. From the point of view of formal languages, this is immediately a problem, since syntax rules are expected to generate finite statements. A succinct equivalent formulation, which avoids these problems, uses universal quantification:
A similar analysis applies to the disjunction,
which can be rephrased using existential quantification:
Algebraic approaches to quantification It is possible to devise abstract algebras whose models include formal languages with quantification, but progress has been slow and interest in such algebra has been limited. Three approaches have been devised to date: Relation algebra, invented by Augustus De Morgan, and developed by Charles Sanders Peirce, Ernst Schröder, Alfred Tarski, and Tarski's students. Relation algebra cannot represent any formula with quantifiers nested more than three deep. Surprisingly, the models of relation algebra include the axiomatic set theory ZFC and Peano arithmetic; Cylindric algebra, devised by Alfred Tarski, Leon Henkin, and others; The polyadic algebra of Paul Halmos.
Notation The two most common quantifiers are the universal quantifier and the existential quantifier. The traditional symbol for the universal quantifier is "∀", a rotated letter "A", which stands for "for all" or "all". The corresponding symbol for the existential quantifier is "∃", a rotated letter "E", which stands for "there exists" or "exists".
An example of translating a quantified statement in a natural language such as English would be as follows. Given the statement, "Each of Peter's friends either likes to dance or likes to go to the beach (or both)", key aspects can be identified and rewritten using symbols including quantifiers. So, let X be the set of all Peter's friends, P(x) the predicate "x likes to dance", and Q(x) the predicate "x likes to go to the beach". Then the above sentence can be written in formal notation as , which is read, "for every x that is a member of X, P applies to x or Q applies to x".
Some other quantified expressions are constructed as follows,
for a formula P. These two expressions (using the definitions above) are read as "there exists a friend of Peter who likes to dance" and "all friends of Peter like to dance", respectively. Variant notations include, for set X and set members x:
All of these variations also apply to universal quantification. Other variations for the universal quantifier are
Some versions of the notation explicitly mention the range of quantification. The range of quantification must always be specified; for a given mathematical theory, this can be done in several ways: Assume a fixed domain of discourse for every quantification, as is done in Zermelo–Fraenkel set theory. Fix several domains of discourse in advance and require that each variable have a declared domain, which is the type of that variable. This is analogous to the situation in statically typed computer programming languages, where variables have declared types. Mention explicitly the range of quantification, perhaps using a symbol for the set of all objects in that domain (or the type of the objects in that domain).
One can use any variable as a quantified variable in place of any other, under certain restrictions in which variable capture does not occur. Even if the notation uses typed variables, variables of that type may be used.
Informally or in natural language, the "∀x" or "∃x" might appear after or in the middle of P(x). Formally, however, the phrase that introduces the dummy variable is placed in front.
Mathematical formulas mix symbolic expressions for quantifiers with natural language quantifiers such as,
Keywords for uniqueness quantification include:
Further, x may be replaced by a pronoun. For example,
Order of quantifiers (nesting)
The order of quantifiers is critical to meaning, as is illustrated by the following two propositions:
This is clearly true; it just asserts that every natural number has a square. The meaning of the assertion in which the order of quantifiers is reversed is different:
This is clearly false; it asserts that there is a single natural number s that is the square of every natural number. This is because the syntax directs that any variable cannot be a function of subsequently introduced variables.
A less trivial example from mathematical analysis regards the concepts of uniform and pointwise continuity, whose definitions differ only by an exchange in the positions of two quantifiers. A function f from R to R is called
Pointwise continuous if Uniformly continuous if
In the former case, the particular value chosen for δ can be a function of both ε and x, the variables that precede it. In the latter case, δ can be a function only of ε (i.e., it has to be chosen independent of x). For example, f(x) = x2 satisfies pointwise, but not uniform continuity (its slope is unbounded). In contrast, interchanging the two initial universal quantifiers in the definition of pointwise continuity does not change the meaning.
As a general rule, swapping two adjacent universal quantifiers with the same scope (or swapping two adjacent existential quantifiers with the same scope) doesn't change the meaning of the formula (see Example here), but swapping an existential quantifier and an adjacent universal quantifier may change its meaning.
The maximum depth of nesting of quantifiers in a formula is called its "quantifier rank".
Equivalent expressions If D is a domain of x and P(x) is a predicate dependent on object variable x, then the universal proposition can be expressed as
This notation is known as restricted or relativized or bounded quantification. Equivalently one can write,
The existential proposition can be expressed with bounded quantification as
or equivalently
Together with negation, only one of either the universal or existential quantifier is needed to perform both tasks:
which shows that to disprove a "for all x" proposition, one needs no more than to find an x for which the predicate is false. Similarly,
to disprove a "there exists an x" proposition, one needs to show that the predicate is false for all x.
In classical logic, every formula is logically equivalent to a formula in prenex normal form, that is, a string of quantifiers and bound variables followed by a quantifier-free formula.
Quantifier elimination
Range of quantification Every quantification involves one specific variable and a domain of discourse or range of quantification of that variable. The range of quantification specifies the set of values that the variable takes. In the examples above, the range of quantification is the set of natural numbers. Specification of the range of quantification allows us to express the difference between, say, asserting that a predicate holds for some natural number or for some real number. Expository conventions often reserve some variable names such as "n" for natural numbers, and "x" for real numbers, although relying exclusively on naming conventions cannot work in general, since ranges of variables can change in the course of a mathematical argument.
A universally quantified formula over an empty range (like ) is always vacuously true. Conversely, an existentially quantified formula over an empty range (like ) is always false.
A more natural way to restrict the domain of discourse uses guarded quantification. For example, the guarded quantification
means
In some mathematical theories, a single domain of discourse fixed in advance is assumed. For example, in Zermelo–Fraenkel set theory, variables range over all sets. In this case, guarded quantifiers can be used to mimic a smaller range of quantification. Thus in the example above, to express
in Zermelo–Fraenkel set theory, one would write
where N is the set of all natural numbers.
Formal semantics Mathematical semantics is the application of mathematics to study the meaning of expressions in a formal language. It has three elements: a mathematical specification of a class of objects via syntax, a mathematical specification of various semantic domains and the relation between the two, which is usually expressed as a function from syntactic objects to semantic ones. This article only addresses the issue of how quantifier elements are interpreted. The syntax of a formula can be given by a syntax tree. A quantifier has a scope, and an occurrence of a variable x is free if it is not within the scope of a quantification for that variable. Thus in
the occurrence of both x and y in C(y, x) is free, while the occurrence of x and y in B(y, x) is bound (i.e. non-free).
An interpretation for first-order predicate calculus assumes as given a domain of individuals X. A formula A whose free variables are x1, ..., xn is interpreted as a Boolean-valued function F(v1, ..., vn) of n arguments, where each argument ranges over the domain X. Boolean-valued means that the function assumes one of the values T (interpreted as truth) or F (interpreted as falsehood). The interpretation of the formula
is the function G of n-1 arguments such that G(v1, ..., vn-1) = T if and only if F(v1, ..., vn-1, w) = T for every w in X. If F(v1, ..., vn-1, w) = F for at least one value of w, then G(v1, ..., vn-1) = F. Similarly the interpretation of the formula
is the function H of n-1 arguments such that H(v1, ..., vn-1) = T if and only if F(v1, ..., vn-1, w) = T for at least one w and H(v1, ..., vn-1) = F otherwise.
The semantics for uniqueness quantification requires first-order predicate calculus with equality. This means there is given a distinguished two-placed predicate "="; the semantics is also modified accordingly so that "=" is always interpreted as the two-place equality relation on X. The interpretation of
then is the function of n-1 arguments, which is the logical and of the interpretations of