View source for Quantifier (logic)

{{Short description|Mathematical use of "for all" and "there exists"}}
{{Other uses|Quantifier (disambiguation)}}
{{Lead rewrite|date=August 2022}}

In [[mathematical logic|logic]], a '''quantifier''' is an operator that specifies how many individuals in the [[domain of discourse]] satisfy an [[open formula]]. For instance, the [[universal quantifier]] <math> \forall </math> in the [[first order logic|first order]] formula <math> \forall x P(x)</math> expresses that everything in the domain satisfies the property denoted by <math>P</math>. On the other hand, the [[existential quantifier]] <math> \exists </math> in the formula <math> \exists x P(x)</math> expresses that there exists something in the domain which satisfies that property. A formula where a quantifier takes widest [[scope (logic)|scope]] is called a quantified formula. A quantified formula must contain a [[Free variables and bound variables|bound variable]] and a [[subformula]] specifying a property of the referent of that variable.

The most commonly used quantifiers are <math>\forall</math> and <math>\exists</math>. These quantifiers are standardly defined as [[Dual (mathematics)|dual]]s; in [[classical logic]], they are interdefinable using [[negation]]. They can also be used to define more complex quantifiers, as in the formula <math> \neg \exists x P(x)</math> which expresses that nothing has the property <math>P</math>. Other quantifiers are only definable within [[second order logic]] or [[higher order logic]]s. Quantifiers have been generalized beginning with the work of [[Andrzej Mostowski|Mostowski]] and [[Per Lindström|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, while the exchange of quantifications in different types changes the meaning. As an example, the only difference in the definition of [[Uniform continuity#Definition of uniform continuity|uniform continuity]] and [[Uniform continuity#Definition of (ordinary) continuity|(ordinary) continuity]] is the order of quantifications.

First order quantifiers approximate the meanings of some [[natural language]] quantifiers such as "some" and "all". However, many natural language quantifiers can only be analyzed in terms of [[generalized quantifier]]s.

==Relations to logical conjunction and disjunction==
For a finite domain of discourse <math>D = \{a_1,...a_n\}</math>, the universally quantified formula <math>\forall x \in D \; P(x)</math> is equivalent to the [[logical conjunction]] <math>P(a_1) \land ... \land P(a_n)</math>. 
Dually, the existentially quantified formula <math>\exists x \in D \; P(x)</math> is equivalent to the [[logical disjunction]] <math>P(a_1) \lor ... \lor P(a_n)</math>. 
For example, if <math>B = \{ 0,1 \}</math> is the set of [[binary digit]]s, the formula <math>\forall x \in B \; x = x^2</math> abbreviates <math>0 = 0^2 \land 1 = 1^2</math>, which evaluates to ''true''.

===Infinite domain of discourse===

Consider the following statement (''using dot notation for multiplication''):
: 1 · 2 = 1 + 1, and 2 · 2 = 2 + 2, and 3 · 2 = 3 + 3, ..., and 100 · 2 = 100 + 100, and ..., etc.
This has the appearance of an ''infinite [[logical conjunction|conjunction]]'' of propositions. From the point of view of [[formal language]]s, this is immediately a problem, since [[Syntax (logic)|syntax]] rules are expected to generate [[finite set|finite]] words.

The example above is fortunate in that there is a [[Algorithm|procedure]] to generate all the conjuncts.  However, if an assertion were to be made about every [[irrational number]], there would be no way to enumerate all the conjuncts, since irrationals cannot be enumerated. A succinct, equivalent formulation which avoids these problems uses ''universal quantification'':
: For each [[natural number]] ''n'', ''n'' · 2 = ''n'' + ''n''.
A similar analysis applies to the [[disjunction (logic)|disjunction]],
: 1 is equal to 5 + 5, or 2 is equal to 5 + 5, or 3 is equal to 5 + 5, ... , or 100 is equal to 5 + 5, or ..., etc.
which can be rephrased using ''existential quantification'':
: For some [[natural number]] ''n'', ''n'' is equal to 5+5.

==Algebraic approaches to quantification==
It is possible to devise [[abstract algebra]]s whose [[model theory|models]] include [[formal language]]s with quantification, but progress has been slow{{clarify|date=October 2016}} 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 (mathematician)|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".<ref>{{Cite web|title=Predicates and Quantifiers|url=https://www.csm.ornl.gov/~sheldon/ds/sec1.6.html|access-date=2020-09-04|website=www.csm.ornl.gov}}</ref><ref>{{Cite web|title=1.2 Quantifiers|url=https://www.whitman.edu/mathematics/higher_math_online/section01.02.html|access-date=2020-09-04|website=www.whitman.edu}}</ref>

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 (mathematical logic)|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 <math> \forall{x}{\in}X, (P(x) \lor Q(x)) </math>, which is read, "for every ''x'' that is a member of ''X'', ''P'' applies to ''x'' [[inclusive or|or]] ''Q'' applies to ''x''".

Some other quantified expressions are constructed as follows, 
: <math> \exists{x}\, P</math><ref>{{cite book | author=K.R. Apt | contribution=Logic Programming | pages=493&ndash;574 | isbn=0-444-88074-7 | editor=Jan van Leeuwen | title=Formal Models and Semantics | publisher=Elsevier | series=Handbook of Theoretical Computer Science | volume=B | year=1990}} Here: p.497</ref> &nbsp; &nbsp; <math>\forall{x}\, P </math>
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'':
: <math> \bigvee_{x} P</math> &nbsp; &nbsp; <math>(\exists{x}) P</math><ref>{{Cite book|last1=Schwichtenberg|first1=Helmut|url=http://dx.doi.org/10.1017/cbo9781139031905|title=Proofs and Computations|last2=Wainer|first2=Stanley S.|date=2009|publisher=Cambridge University Press|isbn=978-1-139-03190-5|location=Cambridge|doi=10.1017/cbo9781139031905 }}</ref> &nbsp; &nbsp; <math>(\exists x \ . \ P)</math> &nbsp; &nbsp; <math>\exists x \ \cdot \ P</math> &nbsp; &nbsp; <math>(\exists x : P)</math> &nbsp; &nbsp; <math>\exists{x}(P)</math><ref>{{cite book | isbn=0-201-02988-X | author=John E. Hopcroft and Jeffrey D. Ullman | title=Introduction to Automata Theory, Languages, and Computation | location=Reading/MA | publisher=Addison-Wesley | year=1979 }} Here: p.p.344</ref> &nbsp; &nbsp; <math>\exists_{x}\, P</math> &nbsp; &nbsp; <math>\exists{x}{,}\, P</math> &nbsp; &nbsp; <math>\exists{x}{\in}X \, P </math> &nbsp; &nbsp; <math>\exists\, x{:}X \, P</math>
All of these variations also apply to universal quantification.
Other variations for the universal quantifier are
: <math>\bigwedge_{x} P</math>{{citation needed|reason=Give an example citation for each notation|date=January 2021}} &nbsp; &nbsp; <math>\bigwedge x P</math><ref>{{cite book | issn=1431-4657 | isbn=3540058192 | author=Hans Hermes | title=Introduction to Mathematical Logic | location=London | publisher=Springer | series=Hochschultext (Springer-Verlag) | year=1973 }} Here: Def. II.1.5</ref> &nbsp; &nbsp; <math>(x) \, P</math><ref>{{Cite journal|last1=Glebskii|first1=Yu. V.|last2=Kogan|first2=D. I.|last3=Liogon'kii|first3=M. I.|last4=Talanov|first4=V. A.|date=1972|title=Range and degree of realizability of formulas in the restricted predicate calculus|url=http://dx.doi.org/10.1007/bf01071084|journal=Cybernetics|volume=5|issue=2|pages=142–154|doi=10.1007/bf01071084|s2cid=121409759 |issn=0011-4235}}</ref>

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 [[Type system|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 (type theory)|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,
: For every natural number ''x'', ...
: There exists an ''x'' such that ...
: For at least one ''x, ....''

Keywords for [[uniqueness quantification]] include:
: For exactly one natural number ''x'', ...
: There is one and only one ''x'' such that ....
Further, ''x'' may be replaced by a [[pronoun]]. For example, 
:For every natural number, its product with 2 equals to its sum with itself.
:Some natural number is prime.

==Order of quantifiers (nesting)==
{{See also|Quantifier shift|}}

The order of quantifiers is critical to meaning, as is illustrated by the following two propositions:
:For every natural number ''n'', there exists a natural number ''s'' such that ''s'' = ''n''<sup>2</sup>.
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:
:There exists a natural number ''s'' such that for every natural number ''n'', ''s'' = ''n''<sup>2</sup>.
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 continuity|uniform]] and [[continuous function|pointwise]] continuity, whose definitions differ only by an exchange in the positions of two quantifiers. A function ''f'' from [[real numbers|'''R''']] to '''R''' is called
* Pointwise continuous if <math display="block">\forall \varepsilon > 0 \; \forall x \in \R \; \exists \delta > 0 \; \forall h \in \R \; (|h| < \delta \, \Rightarrow \, |f(x) - f(x + h)| < \varepsilon ) </math>
* Uniformly continuous if <math display="block">\forall \varepsilon > 0 \; \exists \delta > 0 \; \forall x \in \R \; \forall h \in \R \; (|h| < \delta \, \Rightarrow \, |f(x) - f(x + h)| < \varepsilon ) </math>
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'') = ''x''<sup>2</sup> satisfies pointwise, but not uniform continuity (its slope is unbound).
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 (logic)|scope]] (or swapping two adjacent existential quantifiers with the same scope) doesn't change the meaning of the formula (see [[Prenex normal form#Example|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

:<math>\forall x\!\in\!D\; P(x).</math>

This notation is known as restricted or relativized or [[Bounded quantifier|bounded quantification]]. Equivalently one can write,

:<math>\forall x\;(x\!\in\!D \to P(x)).</math>

The existential proposition can be expressed with bounded quantification as

:<math>\exists x\!\in\!D\; P(x),</math>

or equivalently

:<math>\exists x\;(x\!\in\!\!D \land P(x)).</math>

Together with negation, only one of either the universal or existential quantifier is needed to perform both tasks:

:<math>\neg (\forall x\!\in\!D\; P(x)) \equiv \exists x\!\in\!D\; \neg P(x),</math>

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,

:<math>\neg (\exists x\!\in\!D\; P(x)) \equiv \forall x\!\in\!D\; \neg P(x),</math>

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===
{{excerpt|Quantifier elimination}}
==Range of quantification<!--'Range of quantification' redirects here-->==
Every quantification involves one specific variable and a [[domain of discourse]] or '''range of quantification'''<!--boldface per WP:R#PLA--> 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 <math>\forall x\!\in\!\varnothing\; x \neq x</math>) is always [[vacuously true]]. Conversely, an existentially quantified formula over an empty range (like <math>\exists x\!\in\!\varnothing\; x = x</math>) is always false.

A more natural way to restrict the domain of discourse uses ''guarded quantification''.  For example, the guarded quantification 
:For some natural number ''n'', ''n'' is even and ''n'' is prime
means
:For some [[even number]] ''n'', ''n'' is prime.

In some [[Mathematical theory|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
:For every natural number ''n'', ''n''·2 = ''n'' + ''n''
in Zermelo–Fraenkel set theory, one would write
:For every ''n'', if ''n'' belongs to '''N''', then ''n''·2 = ''n'' + ''n'',
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 (logic)|syntax]], a mathematical specification of various [[semantic domain]]s 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 (logic)|scope]], and an occurrence of a variable ''x'' is [[free variable|free]] if it is not within the scope of a quantification for that variable. Thus in
:<math> \forall x (\exists y  B(x,y)) \vee C(y,x) </math>
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).

[[File:QuantifierScopes svg.svg|thumb|350px|Syntax tree of the formula <math> \forall x (\exists y  B(x,y)) \vee C(y,x) </math>, illustrating scope and variable capture. Bound and free variable occurrences are colored in red and green, respectively.]]
An [[interpretation (logic)|interpretation]] for [[first-order predicate calculus]] assumes as given a domain of individuals ''X''.  A formula ''A'' whose free variables are ''x''<sub>1</sub>, ..., ''x''<sub>n</sub> is interpreted as a [[Boolean function|Boolean]]-valued function ''F''(''v''<sub>1</sub>, ..., ''v''<sub>''n''</sub>) 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
:<math> \forall x_n A(x_1, \ldots , x_n) </math>
is the function ''G'' of ''n''-1 arguments such that ''G''(''v''<sub>1</sub>, ..., ''v''<sub>''n''-1</sub>) = '''T''' if and only if ''F''(''v''<sub>1</sub>, ..., ''v''<sub>''n''-1</sub>, ''w'') = '''T''' for every ''w'' in ''X''. If  ''F''(''v''<sub>1</sub>, ..., ''v''<sub>''n''-1</sub>, ''w'') = '''F''' for at least one value of ''w'', then ''G''(''v''<sub>1</sub>, ..., ''v''<sub>''n''-1</sub>) = '''F'''. Similarly the interpretation of the formula
:<math> \exists x_n A(x_1, \ldots , x_n) </math>
is the function ''H'' of ''n''-1 arguments such that ''H''(''v''<sub>1</sub>, ..., ''v''<sub>''n''-1</sub>) = '''T''' if and only if ''F''(''v''<sub>1</sub>, ..., ''v''<sub>''n''-1</sub>, ''w'') = '''T''' for at least one ''w'' and  ''H''(''v''<sub>1</sub>, ..., ''v''<sub>''n''-1</sub>) = '''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  
:<math> \exists !   x_n A(x_1, \ldots , x_n) </math>
then is the function of ''n''-1 arguments, which is the logical ''and'' of the interpretations of 
:<math> \exists  x_n A(x_1, \ldots , x_n) </math>
:<math> \forall y,z \big( A(x_1, \ldots ,x_{n-1}, y) \wedge  A(x_1, \ldots ,x_{n-1}, z) \implies y = z \big).</math>

Each kind of quantification defines a corresponding [[closure operator]] on the set of formulas, by adding, for each free variable ''x'', a quantifier to bind ''x''.<ref>in general, for a quantifer '''Q''', closure makes sense only if the order of '''Q''' quantification does not matter, i.e. if '''Q'''<!------>''x'' '''Q'''<!------>''y'' ''p''(''x'',''y'') is equivalent to '''Q'''<!------>''y'' '''Q'''<!------>''x'' ''p''(''x'',''y''). This is satisfied for '''Q''' ∈ {∀,∃}, cf. [[#Order of quantifiers (nesting)]] above.</ref> For example, the ''existential closure'' of the [[open formula]] ''n''>2 ∧ ''x''<sup>''n''</sup>+''y''<sup>''n''</sup>=''z''<sup>''n''</sup> is the closed formula ∃''n'' ∃''x'' ∃''y'' ∃''z'' (''n''>2 ∧ ''x''<sup>''n''</sup>+''y''<sup>''n''</sup>=''z''<sup>''n''</sup>); the latter formula, when interpreted over the positive integers, is known to be false by [[Fermat's Last Theorem]]. As another example, equational axioms, like ''x''+''y''=''y''+''x'', are usually meant to denote their ''universal closure'', like ∀''x'' ∀''y'' (''x''+''y''=''y''+''x'') to express [[commutativity]].

==Paucal, multal and other degree quantifiers==
{{See also|Fubini's theorem|measurable}}

None of the quantifiers previously discussed apply to a quantification such as

:There are many integers ''n'' < 100, such that ''n'' is divisible by 2 or 3 or 5.

One possible interpretation mechanism can be obtained as follows: Suppose that in addition to a semantic domain ''X'', we have given a [[probability measure]] P defined on ''X'' and cutoff numbers 0 < ''a'' ≤ ''b'' ≤  1.  If ''A'' is a formula with free variables ''x''<sub>1</sub>,...,''x''<sub>''n''</sub> whose interpretation is
the function ''F'' of variables ''v''<sub>1</sub>,...,''v''<sub>''n''</sub>
then the interpretation of 
:<math> \exists^{\mathrm{many}} x_n A(x_1, \ldots, x_{n-1}, x_n) </math>
is the function of ''v''<sub>1</sub>,...,''v''<sub>''n''-1</sub> which is '''T''' if and only if
:<math> \operatorname{P} \{w: F(v_1, \ldots, v_{n-1}, w) = \mathbf{T} \} \geq b </math>
and '''F''' otherwise.  Similarly, the interpretation of 
:<math> \exists^{\mathrm{few}}  x_n  A(x_1, \ldots, x_{n-1}, x_n) </math>
is the function of ''v''<sub>1</sub>,...,''v''<sub>''n''-1</sub> which is '''F''' if and only if
:<math> 0< \operatorname{P} \{w: F(v_1, \ldots, v_{n-1}, w) = \mathbf{T}\} \leq a </math>
and '''T''' otherwise.

==Other quantifiers==
A few other quantifiers have been proposed over time. In particular, the solution quantifier,<ref>[[E. C. R. Hehner|Hehner, Eric C. R.]], 2004, [http://www.cs.utoronto.ca/~hehner/aPToP ''Practical Theory of Programming''], 2nd edition, p. 28</ref>{{rp|28}} noted § ([[section sign]]) and read "those". For example,
:<math> \left[ \S n \in \mathbb{N} \quad n^2 \leq 4 \right] = \{0, 1, 2\}</math>
is read "those ''n'' in '''N''' such that ''n''<sup>2</sup> ≤ 4 are in {0,1,2}." The same construct is expressible in [[set-builder notation]] as
:<math>\{n \in \mathbb N: n^2 \le 4\} = \{0, 1, 2\}.</math>
Contrary to the other quantifiers, § yields a set rather than a formula.<ref>Hehner (2004) uses the term "quantifier" in a very general sense, also including e.g. [[summation]].</ref>

Some other quantifiers sometimes used in mathematics include:
*There are infinitely many elements such that...
*For all but finitely many elements... (sometimes expressed as "for [[almost all]] elements...").
*There are uncountably many elements such that...
*For all but countably many elements...
*For all elements in a set of positive measure...
*For all elements except those in a set of measure zero...

==History==
[[Term logic]], also called Aristotelian logic, treats quantification in a manner that is closer to natural language, and also less suited to formal analysis. Term logic treated ''All'', ''Some''  and ''No'' in the 4th century BC, in an account also touching on the [[alethic modalities]].

In 1827, [[George Bentham]] published his ''Outline of a New System of Logic: With a Critical Examination of Dr. Whately's Elements of Logic'', describing the principle of the quantifier, but the book was not widely circulated.<ref>George Bentham, ''Outline of a new system of logic: with a critical examination of Dr. Whately's Elements of Logic'' (1827); Thoemmes; Facsimile edition (1990)  {{isbn|1-85506-029-9}}</ref>

[[File:De Morgan Augustus.jpg|thumb|upright|[[Augustus De Morgan]] (1806–1871) was the first to use "quantifier" in the modern sense.]]
[[Sir William Hamilton, 9th Baronet|William Hamilton]] claimed to have coined the terms "quantify" and "quantification", most likely in his Edinburgh lectures c. 1840. [[Augustus De Morgan]] confirmed this in 1847, but modern usage began with De Morgan in 1862 where he makes statements such as "We are to take in both ''all'' and ''some-not-all'' as quantifiers".<ref>{{cite book|last1=Peters|first1=Stanley|last2=Westerståhl|first2=Dag|title=Quantifiers in Language and Logic|url=https://books.google.com/books?id=PrYUDAAAQBAJ&pg=PA34|date=2006-04-27|publisher=Clarendon Press|isbn=978-0-19-929125-0|pages=34–}}</ref>

[[Gottlob Frege]], in his 1879 ''[[Begriffsschrift]]'', was the first to employ a quantifier to bind a variable ranging over a [[domain of discourse]] and appearing in [[Predicate (mathematical logic)|predicate]]s. He would universally quantify a variable (or relation) by writing the variable over a dimple in an otherwise straight line appearing in his diagrammatic formulas. Frege did not devise an explicit notation for existential quantification, instead employing his equivalent of ~∀''x''~, or [[contraposition]]. Frege's treatment of quantification went largely unremarked until [[Bertrand Russell]]'s 1903 ''Principles of Mathematics''.

In work that culminated in Peirce (1885), [[Charles Sanders Peirce]] and his student [[Oscar Howard Mitchell]] independently invented universal and existential quantifiers, and [[bound variable]]s. Peirce and Mitchell wrote Π<sub>x</sub> and Σ<sub>x</sub> where we now write ∀''x'' and ∃''x''. Peirce's notation can be found in the writings of [[Ernst Schröder (mathematician)|Ernst Schröder]], [[Leopold Loewenheim]], [[Thoralf Skolem]], and Polish logicians into the 1950s. Most notably, it is the notation of [[Kurt Gödel]]'s landmark 1930 paper on the [[Gödel's completeness theorem|completeness]] of [[first-order logic]], and 1931 paper on the [[Gödel's incompleteness theorem|incompleteness]] of [[Peano arithmetic]].

Peirce's approach to quantification also influenced [[William Ernest Johnson]] and [[Giuseppe Peano]], who invented yet another notation, namely (''x'') for the universal quantification of ''x'' and (in 1897) ∃''x'' for the existential quantification of ''x''. Hence for decades, the canonical notation in philosophy and mathematical logic was (''x'')''P'' to express "all individuals in the domain of discourse have the property ''P''," and "(∃''x'')''P''" for "there exists at least one individual in the domain of discourse having the property ''P''." Peano, who was much better known than Peirce, in effect diffused the latter's thinking throughout Europe. Peano's notation was adopted by the ''[[Principia Mathematica]]'' of [[Alfred North Whitehead|Whitehead]] and [[Bertrand Russell|Russell]], [[Willard Van Orman Quine|Quine]], and [[Alonzo Church]]. In 1935, [[Gentzen]] introduced the ∀ symbol, by analogy with Peano's ∃ symbol. ∀ did not become canonical until the 1960s.

Around 1895, Peirce began developing his [[existential graph]]s, whose variables can be seen as tacitly quantified. Whether the shallowest instance of a variable is even or odd determines whether that variable's quantification is universal or existential. (Shallowness is the contrary of depth, which is determined by the nesting of negations.) Peirce's graphical logic has attracted some attention in recent years by those researching [[heterogeneous reasoning]] and [[logical graph|diagrammatic inference]].

==See also==
{{Portal|Philosophy}}
*[[Absolute generality]]
*[[Almost all]]
*[[Branching quantifier]]
*[[Conditional quantifier]]
*[[Counting quantification]]
*[[Eventually (mathematics)]]
*[[Generalized quantifier]] &mdash; a higher-order property used as standard semantics of quantified [[noun phrases]]
*[[Lindström quantifier]] &mdash; a generalized polyadic quantifier
*[[Quantifier shift]]

==References==
{{Reflist}}

== Bibliography ==
* [[Jon Barwise|Barwise, Jon]]; and [[John Etchemendy|Etchemendy, John]], 2000. ''Language Proof and Logic''. CSLI (University of Chicago Press) and New York: Seven Bridges Press. A gentle introduction to [[first-order logic]] by two first-rate logicians.
*{{cite web
 |last= Brown
 |first= Christopher W.
 |date= July 31, 2002
 |url= https://www.usna.edu/CS/qepcadweb/B/QE.html
 |title= What is Quantifier Elimination
 |access-date= Aug 30, 2018
}}
* [[Gottlob Frege|Frege, Gottlob]], 1879. ''[[Begriffsschrift]]''. Translated in [[Jean van Heijenoort]], 1967. ''From Frege to Gödel: A Source Book on Mathematical Logic, 1879-1931''. Harvard University Press. The first appearance of quantification.
* [[David Hilbert|Hilbert, David]]; and [[Wilhelm Ackermann|Ackermann, Wilhelm]], 1950 (1928). ''[[Principles of Mathematical Logic]]''. Chelsea. Translation of ''Grundzüge der theoretischen Logik''. Springer-Verlag. The 1928 first edition is the first time quantification was consciously employed in the now-standard  manner, namely as binding variables ranging over some fixed domain of discourse. This is the defining aspect of [[first-order logic]].
* [[Charles Sanders Peirce|Peirce, C. S.]], 1885, "On the Algebra of Logic: A Contribution to the Philosophy of Notation, ''American Journal of Mathematics'', Vol. 7, pp. 180–202. Reprinted in Kloesel, N. ''et al.'', eds., 1993. ''Writings of C. S. Peirce, Vol. 5''. Indiana University Press. The first appearance of quantification in anything like its present form.
* [[Hans Reichenbach|Reichenbach, Hans]], 1975 (1947). ''Elements of Symbolic Logic'', Dover Publications. The quantifiers are discussed in chapters §18 "Binding of variables" through §30 "Derivations from Synthetic Premises".
* Westerståhl, Dag, 2001, "Quantifiers," in Goble, Lou, ed., ''The Blackwell Guide to Philosophical Logic''. Blackwell.
* Wiese, Heike, 2003. ''Numbers, language, and the human mind''. Cambridge University Press. {{isbn|0-521-83182-2}}.<!---may be irrelevant here?--->

==External links==
{{Wiktionary|quantification}}
* {{springer|title=Quantifier|id=p/q076260}}
* {{cite web|url= http://www.math.hawaii.edu/~ramsey/Logic/ForAll.html|title= "For all" and "there exists" topical phrases, sentences and expressions|archive-url= https://web.archive.org/web/20000301144835/http://www.math.hawaii.edu/~ramsey/Logic/ForAll.html|archive-date= March 1, 2000|url-status= dead}}. From College of Natural Sciences, [[University of Hawaii at Manoa]].
* [[Stanford Encyclopedia of Philosophy]]:
** Shapiro, Stewart (2000). [http://plato.stanford.edu/entries/logic-classical/ "Classical Logic"] (Covers syntax, model theory, and metatheory for first order logic in the natural deduction style.)
** Westerståhl, Dag (2005). [http://plato.stanford.edu/entries/generalized-quantifiers/ "Generalized quantifiers"]
* Peters, Stanley; Westerståhl, Dag (2002). [http://www.stanford.edu/group/nasslli/courses/peters-wes/PWbookdraft2-3.pdf "Quantifiers"] {{Webarchive|url=https://web.archive.org/web/20120716183245/http://www.stanford.edu/group/nasslli/courses/peters-wes/PWbookdraft2-3.pdf |date=2012-07-16 }}

{{Formal Fallacy}}
{{Mathematical logic}}
{{Formal semantics}}
{{Authority control}}

[[Category:Logic]]
[[Category:Predicate logic]]
[[Category:Quantifier (logic)]]
[[Category:Philosophical logic]]
[[Category:Semantics]]