Universal quantification

Last updated
Universal quantification
Type Quantifier
Field Mathematical logic
Statement is true when is true for all values of .
Symbolic statement

In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any", "for all", or "for any". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other words, it is the predication of a property or relation to every member of the domain. It asserts that a predicate within the scope of a universal quantifier is true of every value of a predicate variable.

Contents

It is usually denoted by the turned A (∀) logical operator symbol, which, when used together with a predicate variable, is called a universal quantifier ("x", "∀(x)", or sometimes by "(x)" alone). Universal quantification is distinct from existential quantification ("there exists"), which only asserts that the property or relation holds for at least one member of the domain.

Quantification in general is covered in the article on quantification (logic). The universal quantifier is encoded as U+2200FOR ALL in Unicode, and as \forall in LaTeX and related formula editors.

Basics

Suppose it is given that

2·0 = 0 + 0, and 2·1 = 1 + 1, and 2·2 = 2 + 2, etc.

This would seem to be a logical conjunction because of the repeated use of "and". However, the "etc." cannot be interpreted as a conjunction in formal logic. Instead, the statement must be rephrased:

For all natural numbers n, one has 2·n = n + n.

This is a single statement using universal quantification.

This statement can be said to be more precise than the original one. While the "etc." informally includes natural numbers, and nothing more, this was not rigorously given. In the universal quantification, on the other hand, the natural numbers are mentioned explicitly.

This particular example is true, because any natural number could be substituted for n and the statement "2·n = n + n" would be true. In contrast,

For all natural numbers n, one has 2·n > 2 + n

is false, because if n is substituted with, for instance, 1, the statement "2·1 > 2 + 1" is false. It is immaterial that "2·n > 2 + n" is true for most natural numbers n: even the existence of a single counterexample is enough to prove the universal quantification false.

On the other hand, for all composite numbers n, one has 2·n > 2 + n is true, because none of the counterexamples are composite numbers. This indicates the importance of the domain of discourse , which specifies which values n can take. [note 1] In particular, note that if the domain of discourse is restricted to consist only of those objects that satisfy a certain predicate, then for universal quantification this requires a logical conditional. For example,

For all composite numbers n, one has 2·n > 2 + n

is logically equivalent to

For all natural numbers n, if n is composite, then 2·n > 2 + n.

Here the "if ... then" construction indicates the logical conditional.

Notation

In symbolic logic, the universal quantifier symbol (a turned "A" in a sans-serif font, Unicode U+2200) is used to indicate universal quantification. It was first used in this way by Gerhard Gentzen in 1935, by analogy with Giuseppe Peano's (turned E) notation for existential quantification and the later use of Peano's notation by Bertrand Russell. [1]

For example, if P(n) is the predicate "2·n > 2 + n" and N is the set of natural numbers, then

is the (false) statement

"for all natural numbers n, one has 2·n > 2 + n".

Similarly, if Q(n) is the predicate "n is composite", then

is the (true) statement

"for all natural numbers n, if n is composite, then n > 2 + n".

Several variations in the notation for quantification (which apply to all forms) can be found in the Quantifier article.

Properties


Negation

The negation of a universally quantified function is obtained by changing the universal quantifier into an existential quantifier and negating the quantified formula. That is,

where denotes negation.

For example, if P(x) is the propositional function "x is married", then, for the set X of all living human beings, the universal quantification

Given any living person x, that person is married

is written

This statement is false. Truthfully, it is stated that

It is not the case that, given any living person x, that person is married

or, symbolically:

.

If the function P(x) is not true for every element of X, then there must be at least one element for which the statement is false. That is, the negation of is logically equivalent to "There exists a living person x who is not married", or:

It is erroneous to confuse "all persons are not married" (i.e. "there exists no person who is married") with "not all persons are married" (i.e. "there exists a person who is not married"):

Other connectives

The universal (and existential) quantifier moves unchanged across the logical connectives , , , and , as long as the other operand is not affected; that is:

Conversely, for the logical connectives , , , and , the quantifiers flip:

Rules of inference

A rule of inference is a rule justifying a logical step from hypothesis to conclusion. There are several rules of inference which utilize the universal quantifier.

Universal instantiation concludes that, if the propositional function is known to be universally true, then it must be true for any arbitrary element of the universe of discourse. Symbolically, this is represented as

where c is a completely arbitrary element of the universe of discourse.

Universal generalization concludes the propositional function must be universally true if it is true for any arbitrary element of the universe of discourse. Symbolically, for an arbitrary c,

The element c must be completely arbitrary; else, the logic does not follow: if c is not arbitrary, and is instead a specific element of the universe of discourse, then P(c) only implies an existential quantification of the propositional function.

The empty set

By convention, the formula is always true, regardless of the formula P(x); see vacuous truth.

Universal closure

The universal closure of a formula φ is the formula with no free variables obtained by adding a universal quantifier for every free variable in φ. For example, the universal closure of

is

.

As adjoint

In category theory and the theory of elementary topoi, the universal quantifier can be understood as the right adjoint of a functor between power sets, the inverse image functor of a function between sets; likewise, the existential quantifier is the left adjoint. [2]

For a set , let denote its powerset. For any function between sets and , there is an inverse image functor between powersets, that takes subsets of the codomain of f back to subsets of its domain. The left adjoint of this functor is the existential quantifier and the right adjoint is the universal quantifier .

That is, is a functor that, for each subset , gives the subset given by

those in the image of under . Similarly, the universal quantifier is a functor that, for each subset , gives the subset given by

those whose preimage under is contained in .

The more familiar form of the quantifiers as used in first-order logic is obtained by taking the function f to be the unique function so that is the two-element set holding the values true and false, a subset S is that subset for which the predicate holds, and

which is true if is not empty, and

which is false if S is not X.

The universal and existential quantifiers given above generalize to the presheaf category.

See also

Notes

  1. Further information on using domains of discourse with quantified statements can be found in the Quantification (logic) article.

Related Research Articles

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

<span class="mw-page-title-main">Original proof of Gödel's completeness theorem</span>

The proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 is not easy to read today; it uses concepts and formalisms that are no longer used and terminology that is often obscure. The version given below attempts to represent all the steps in the proof and all the important ideas faithfully, while restating the proof in the modern language of mathematical logic. This outline should not be considered a rigorous proof of the theorem.

In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a canonical normal form, it is useful in automated theorem proving and circuit theory.

In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, when used together with a predicate variable, is called an existential quantifier ("x" or "∃(x)" or "(∃x)"). Existential quantification is distinct from universal quantification ("for all"), which asserts that the property or relation holds for all members of the domain. Some sources use the term existentialization to refer to existential quantification.

In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as Russell's paradox. Today, Zermelo–Fraenkel set theory, with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics. Zermelo–Fraenkel set theory with the axiom of choice included is abbreviated ZFC, where C stands for "choice", and ZF refers to the axioms of Zermelo–Fraenkel set theory with the axiom of choice excluded.

<span class="mw-page-title-main">Negation</span> Logical operation

In logic, negation, also called the logical complement, is an operation that takes a proposition to another proposition "not ", written , or . It is interpreted intuitively as being true when is false, and false when is true. Negation is thus a unary logical connective. It may be applied as an operation on notions, propositions, truth values, or semantic values more generally. In classical logic, negation is normally identified with the truth function that takes truth to falsity. In intuitionistic logic, according to the Brouwer–Heyting–Kolmogorov interpretation, the negation of a proposition is the proposition whose proofs are the refutations of .

<span class="mw-page-title-main">Indicator function</span> Mathematical function characterizing set membership

In mathematics, an indicator function or a characteristic function of a subset of a set is a function that maps elements of the subset to one, and all other elements to zero. That is, if A is a subset of some set X, one has if and otherwise, where is a common notation for the indicator function. Other common notations are and

A formula of the predicate calculus is in prenex normal form (PNF) if it is written as a string of quantifiers and bound variables, called the prefix, followed by a quantifier-free part, called the matrix. Together with the normal forms in propositional logic, it provides a canonical normal form useful in automated theorem proving.

In the foundations of mathematics, von Neumann–Bernays–Gödel set theory (NBG) is an axiomatic set theory that is a conservative extension of Zermelo–Fraenkel–choice set theory (ZFC). NBG introduces the notion of class, which is a collection of sets defined by a formula whose quantifiers range only over sets. NBG can define classes that are larger than sets, such as the class of all sets and the class of all ordinals. Morse–Kelley set theory (MK) allows classes to be defined by formulas whose quantifiers range over classes. NBG is finitely axiomatizable, while ZFC and MK are not.

Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized. It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers, which determine if a given artifact possesses safety or liveness properties. For example, CTL can specify that when some initial condition is satisfied, then all possible executions of a program avoid some undesirable condition. In this example, the safety property could be verified by a model checker that explores all possible transitions out of program states satisfying the initial condition and ensures that all such executions satisfy the property. Computation tree logic belongs to a class of temporal logics that includes linear temporal logic (LTL). Although there are properties expressible only in CTL and properties expressible only in LTL, all properties expressible in either logic can also be expressed in CTL*.

In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories (Rathjen 2005).

Independence-friendly logic is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form and , where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic.

In mathematical logic, a tautology is a formula or assertion that is true in every possible interpretation. An example is "x=y or x≠y". Similarly, "either the ball is green, or the ball is not green" is always true, regardless of the colour of the ball.

Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.

An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation. The general study of interpretations of formal languages is called formal semantics.

In mathematical logic, predicate functor logic (PFL) is one of several ways to express first-order logic by purely algebraic means, i.e., without quantified variables. PFL employs a small number of algebraic devices called predicate functors that operate on terms to yield terms. PFL is mostly the invention of the logician and philosopher Willard Quine.

In mathematical logic the theory of pure equality is a first-order theory. It has a signature consisting of only the equality relation symbol, and includes no non-logical axioms at all.

Dependence logic is a logical formalism, created by Jouko Väänänen, which adds dependence atoms to the language of first-order logic. A dependence atom is an expression of the form , where are terms, and corresponds to the statement that the value of is functionally dependent on the values of .

In 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 in the first order formula expresses that everything in the domain satisfies the property denoted by . On the other hand, the existential quantifier in the formula expresses that there exists something in the domain which satisfies that property. A formula where a quantifier takes widest scope is called a quantified formula. A quantified formula must contain a bound variable and a subformula specifying a property of the referent of that variable.

In computer science and mathematics, more precisely in automata theory, model theory and formal language, a regular numerical predicate is a kind of relation over integers. Regular numerical predicates can also be considered as a subset of for some arity . One of the main interests of this class of predicates is that it can be defined in plenty of different ways, using different logical formalisms. Furthermore, most of the definitions use only basic notions, and thus allows to relate foundations of various fields of fundamental computer science such as automata theory, syntactic semigroup, model theory and semigroup theory.

References

  1. Miller, Jeff. "Earliest Uses of Symbols of Set Theory and Logic". Earliest Uses of Various Mathematical Symbols.
  2. Saunders Mac Lane, Ieke Moerdijk, (1992) Sheaves in Geometry and Logic Springer-Verlag. ISBN   0-387-97710-4 See page 58