 | This article'slead sectionmay need to be rewritten. Please review thelead guide and helpimprove the lead of this article if you can.(August 2022) (Learn how and when to remove this message) |
Inlogic, aquantifier is an operator that specifies how many individuals in thedomain of discourse satisfy anopen formula. For instance, theuniversal quantifier in thefirst-order formula expresses that everything in the domain satisfies the property denoted by. On the other hand, theexistential quantifier in the formula expresses that there exists something in the domain which satisfies that property. A formula where a quantifier takes widestscope is called a quantified formula. A quantified formula must contain abound variable and asubformula specifying a property of the referent of that variable.
The most commonly used quantifiers are and. These quantifiers are standardly defined asduals; inclassical logic: each can be defined in terms of the other usingnegation. They can also be used to define more complex quantifiers, as in the formula which expresses that nothing has the property. Other quantifiers are only definable withinsecond-order logic orhigher-order logics. Quantifiers have been generalized beginning with the work ofAndrzej Mostowski andPer 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 ofuniform continuity and(ordinary) continuity is the order of quantifications.
First-order quantifiers approximate the meanings of somenatural language quantifiers such as "some" and "all". However, many natural language quantifiers can only be analyzed in terms ofgeneralized quantifiers.
For a finite domain of discourse, the universally quantified formula is equivalent to thelogical conjunction. Dually, the existentially quantified formula is equivalent to thelogical disjunction. For example, if is the set ofbinary digits, the formula abbreviates, which evaluates totrue.
Consider the following statement (using dot notation for multiplication):
This has the appearance of aninfiniteconjunction of propositions. From the point of view offormal languages, this is immediately a problem, sincesyntax rules are expected to generatefinite statements. A succinct equivalent formulation, which avoids these problems, usesuniversal quantification:
A similar analysis applies to thedisjunction,
which can be rephrased usingexistential quantification:
It is possible to deviseabstract algebras whosemodels includeformal languages with quantification, but progress has been slow[clarification needed] and interest in such algebra has been limited. Three approaches have been devised to date:
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".[1][2]
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, letX be the set of all Peter's friends,P(x) thepredicate "x likes to dance", andQ(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 everyx that is a member ofX,P applies toxorQ applies tox".
Some other quantified expressions are constructed as follows,
for a formulaP. 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 setX and set membersx:
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:
One can use any variable as a quantified variable in place of any other, under certain restrictions in whichvariable 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 ofP(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 foruniqueness quantification include:
Further,x may be replaced by apronoun. For example,
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 numbers that is the square ofevery natural number. This is because the syntax directs that any variable cannot be a function of subsequently introduced variables.
A less trivial example frommathematical analysis regards the concepts ofuniform andpointwise continuity, whose definitions differ only by an exchange in the positions of two quantifiers. A functionf fromR toR is called
In the former case, the particular value chosen forδ can be a function of bothε andx, the variables that precede it.In the latter case,δ can be a function only ofε (i.e., it has to be chosen independent ofx). 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 samescope (or swapping two adjacent existential quantifiers with the same scope) doesn't change the meaning of the formula (seeExample 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".
IfD is a domain ofx andP(x) is a predicate dependent on object variablex, then the universal proposition can be expressed as
This notation is known as restricted or relativized orbounded 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 allx" proposition, one needs no more than to find anx for which the predicate is false. Similarly,
to disprove a "there exists anx" proposition, one needs to show that the predicate is false for allx.
Inclassical logic, every formula islogically equivalent to a formula inprenex normal form, that is, a string of quantifiers and bound variables followed by a quantifier-free formula.
Quantifier elimination is a concept of simplification used inmathematical logic,model theory, andtheoretical computer science. Informally, a quantified statement " such that ..." can be viewed as a question "When is there an such that ...?", and the statement without quantifiers can be viewed as the answer to that question.[8]
One way of classifyingformulas is by the amount of quantification. Formulas with lessdepth of quantifier alternation are thought of as being simpler, with the quantifier-free formulas as the simplest.
Atheory has quantifier elimination if for every formula, there exists another formula without quantifiers that isequivalent to it (modulo this theory).Every quantification involves one specific variable and adomain of discourse orrange 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 somereal 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 alwaysvacuously true. Conversely, an existentially quantified formula over an empty range (like) is always false.
A more natural way to restrict the domain of discourse usesguarded quantification. For example, the guarded quantification
means
In somemathematical theories, a single domain of discourse fixed in advance is assumed. For example, inZermelo–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
whereN is the set of all natural numbers.
Mathematical semantics is the application ofmathematics to study the meaning of expressions in a formal language. It has three elements: a mathematical specification of a class of objects viasyntax, a mathematical specification of varioussemantic 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 ascope, and an occurrence of a variablex isfree if it is not within the scope of a quantification for that variable. Thus in
the occurrence of bothx andy inC(y,x) is free, while the occurrence ofx andy inB(y,x) is bound (i.e. non-free).
Aninterpretation forfirst-order predicate calculus assumes as given a domain of individualsX. A formulaA whose free variables arex1, ...,xn is interpreted as aBoolean-valued functionF(v1, ...,vn) ofn arguments, where each argument ranges over the domainX. Boolean-valued means that the function assumes one of the valuesT (interpreted as truth) orF (interpreted as falsehood). The interpretation of the formula
is the functionG ofn-1 arguments such thatG(v1, ...,vn-1) =T if and only ifF(v1, ...,vn-1,w) =T for everyw inX. IfF(v1, ...,vn-1,w) =F for at least one value ofw, thenG(v1, ...,vn-1) =F. Similarly the interpretation of the formula
is the functionH ofn-1 arguments such thatH(v1, ...,vn-1) =T if and only ifF(v1, ...,vn-1,w) =T for at least onew andH(v1, ...,vn-1) =F otherwise.
The semantics foruniqueness 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 onX. The interpretation of
then is the function ofn-1 arguments, which is the logicaland of the interpretations of
Each kind of quantification defines a correspondingclosure operator on the set of formulas, by adding, for each free variablex, a quantifier to bindx.[9] For example, theexistential closure of theopen formulan>2 ∧xn+yn=zn is the closed formula ∃n ∃x ∃y ∃z (n>2 ∧xn+yn=zn); the latter formula, when interpreted over the positive integers, is known to be false byFermat's Last Theorem. As another example, equational axioms, likex+y=y+x, are usually meant to denote theiruniversal closure, like ∀x ∀y (x+y=y+x) to expresscommutativity.
None of the quantifiers previously discussed apply to a quantification such as
One possible interpretation mechanism can be obtained as follows: Suppose that in addition to a semantic domainX, we have given aprobability measure P defined onX and cutoff numbers 0 <a ≤b ≤ 1. IfA is a formula with free variablesx1,...,xn whose interpretation isthe functionF of variablesv1,...,vn then the interpretation of
is the function ofv1,...,vn-1 which isT if and only if
andF otherwise. Similarly, the interpretation of
is the function ofv1,...,vn-1 which isF if and only if
andT otherwise.
A few other quantifiers have been proposed over time. In particular, the solution quantifier,[10]: 28 noted § (section sign) and read "those". For example,
is read "thosen inN such thatn2 ≤ 4 are in {0,1,2}." The same construct is expressible inset-builder notation as
Contrary to the other quantifiers, § yields a set rather than a formula.[11]
Some other quantifiers sometimes used in mathematics include:
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 treatedAll,Some andNo in the 4th century BC, in an account also touching on thealethic modalities.
In 1827,George Bentham published hisOutline 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.[12]
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 bothall andsome-not-all as quantifiers".[13]
Gottlob Frege, in his 1879Begriffsschrift, was the first to employ a quantifier to bind a variable ranging over adomain of discourse and appearing inpredicates. 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~, orcontraposition. Frege's treatment of quantification went largely unremarked untilBertrand Russell's 1903Principles of Mathematics.
In work that culminated in Peirce (1885),Charles Sanders Peirce and his studentOscar Howard Mitchell independently invented universal and existential quantifiers, andbound variables. Peirce and Mitchell wrote Πx and Σx where we now write ∀x and ∃x. Peirce's notation can be found in the writings ofErnst Schröder,Leopold Loewenheim,Thoralf Skolem, and Polish logicians into the 1950s. Most notably, it is the notation ofKurt Gödel's landmark 1930 paper on thecompleteness offirst-order logic, and 1931 paper on theincompleteness ofPeano arithmetic.Per Martin-Löf adopted a similar notation for dependent products and sums in hisintuitionistic type theory, which are conceptually related to quantification.
Peirce's approach to quantification also influencedWilliam Ernest Johnson andGiuseppe Peano, who invented yet another notation, namely (x) for the universal quantification ofx and (in 1897) ∃x for the existential quantification ofx. 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 propertyP", and "(∃x)P" for "there exists at least one individual in the domain of discourse having the propertyP". Peano, who was much better known than Peirce, in effect diffused the latter's thinking throughout Europe. Peano's notation was adopted by thePrincipia Mathematica ofWhitehead andRussell,Quine, andAlonzo 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 hisexistential graphs, 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 researchingheterogeneous reasoning anddiagrammatic inference.
| General | |||||||||
|---|---|---|---|---|---|---|---|---|---|
| Theorems (list) and paradoxes | |||||||||
| Logics |
| ||||||||
| Set theory |
| ||||||||
| Formal systems (list), language and syntax |
| ||||||||
| Proof theory | |||||||||
| Model theory | |||||||||
| Computability theory | |||||||||
| Related | |||||||||
| International | |
|---|---|
| National | |
| Other | |
