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.
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+2200∀FOR ALL in Unicode, and as \forall
in LaTeX and related formula editors.
Suppose it is given that
2·0 = 0 + 0, and 2·1 = 1 + 1, and 2·2 = 2 + 2, ..., and 2 · 100 = 100 + 100, and ..., etc.
This would seem to be an infinite 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.
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
Similarly, if Q(n) is the predicate "n is composite", then
is the (true) statement
Several variations in the notation for quantification (which apply to all forms) can be found in the Quantifier article.
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"):
The universal (and existential) quantifier moves unchanged across the logical connectives ∧, ∨, →, and ↚, as long as the other operand is not affected; [2] that is:
Conversely, for the logical connectives ↑, ↓, ↛, and ←, the quantifiers flip:
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.
By convention, the formula is always true, regardless of the formula P(x); see vacuous truth.
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
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. [3]
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.
First-order logic—also called predicate logic, predicate calculus, quantificational logic—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. Rather than propositions such as "all men are mortal", in first-order logic one can have expressions in the form "for all x, if x is a man, then x is mortal"; where "for all x" is a quantifier, x is a variable, and "... is a man" and "... is mortal" are predicates. 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.
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 propositional logic and Boolean algebra, De Morgan's laws, also known as De Morgan's theorem, are a pair of transformation rules that are both valid rules of inference. They are named after Augustus De Morgan, a 19th-century British mathematician. The rules allow the expression of conjunctions and disjunctions purely in terms of each other via negation.
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.
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.
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them. Any set that receives a classification is called arithmetical. The arithmetical hierarchy was invented independently by Kleene (1943) and Mostowski (1946).
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, then 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 mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers.
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.
Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical 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.
In model theory and related areas of mathematics, a type is an object that describes how a element or finite collection of elements in a mathematical structure might behave. More precisely, it is a set of first-order formulas in a language L with free variables x1, x2,..., xn that are true of a set of n-tuples of an L-structure . Depending on the context, types can be complete or partial and they may use a fixed set of constants, A, from the structure . The question of which types represent actual elements of leads to the ideas of saturated models and omitting types.
Axiomatic 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.
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.
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.
{{cite book}}
: CS1 maint: multiple names: authors list (link) (ch. 2)