Quantifier (logic)

In logic, a quantifier is an operator that specifies how many individuals in the domain of discourse satisfy an open formula.

These quantifiers are standardly defined as duals; in classical logic, they are interdefinable using negation.

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 words.

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: It is possible to devise abstract algebras whose models include formal languages with quantification, but progress has been slow[clarification needed] and interest in such algebra has been limited.

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.

Other variations for the universal quantifier are Some versions of the notation explicitly mention the range of quantification.

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.

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.

In contrast, interchanging the two initial universal quantifiers in the definition of pointwise continuity does not change the meaning.

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.

Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science.

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.

For example, the guarded quantification means In some mathematical theories, a single domain of discourse fixed in advance is assumed.

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.

The semantics for uniqueness quantification requires first-order predicate calculus with equality.

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 domain X, we have given a probability measure P defined on X and cutoff numbers 0 < a ≤ b ≤ 1.

The same construct is expressible in set-builder notation as Contrary to the other quantifiers, § yields a set rather than a formula.

Term logic treated All, Some and No in the 4th century BC, in an account also touching on the alethic modalities.

[12] William Hamilton claimed to have coined the terms "quantify" and "quantification", most likely in his Edinburgh lectures c. 1840.

[13] 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 predicates.

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.

Peirce's notation can be found in the writings of Ernst Schröder, Leopold Loewenheim, Thoralf Skolem, and Polish logicians into the 1950s.

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 Whitehead and Russell, Quine, and Alonzo Church.

Around 1895, Peirce began developing his existential graphs, whose variables can be seen as tacitly quantified.

Peirce's graphical logic has attracted some attention in recent years by those researching heterogeneous reasoning and diagrammatic inference.