Bounded quantifier
Encyclopedia
In the study of formal theories in mathematical logic
, bounded quantifiers are often added to a language in addition to the standard quantifiers "∀" and "∃". Bounded quantifiers differ from "∀" and "∃" in that bounded quantifiers restrict the range of the quantified variable. The study of bounded quantifiers is motivated by the fact that determining whether a sentence
with only bounded quantifiers is true is often not as difficult as determining whether an arbitrary sentence is true.
Common examples include "∀x>0", "∃y<0", "∀x ∊ ℝ". Informally "∀x>0" says "for all x where x is larger than 0", "∃y<0" says "there exists a y where y is less than 0" and "∀x ∊ ℝ" says "for all x where x is a real number". For example, "∀x>0 ∃y<0 (x = y2)" says "every positive number is the square of a negative number".
or arithmetic in all finite types would work as well). There are two types of bounded quantifiers:
and 
.
These quantifiers bind the number variable n and contain a numeric term t which may not mention n but which may have other free variables. (By "numeric terms" here we mean terms such as "1 + 1", "2", "2 × 3", "m + 3", etc.)
These quantifiers are defined by the following rules (
denotes formulas):
There are several motivations for these quantifiers.
For example, there is a definition of primality using only bounded quantifiers. A number n is prime if and only if there are not two numbers strictly less than n whose product is n. There is no quantifier-free definition of primality in the language
, however. The fact that there is a bounded quantifier formula defining primality shows that the primality of each number can be computably decided.
In general, a relation on natural numbers is definable by a bounded formula if and only if it is computable in the linear-time hierarchy, which is defined similarly to the polynomial hierarchy
, but with linear time bounds instead of polynomial. Consequently, all predicates definable by a bounded formula are Kalmár elementary, context-sensitive
, and primitive recursive.
In the arithmetical hierarchy
, an arithmetical formula which contains only bounded quantifiers is called
, 
, and 
. The superscript 0 is sometimes omitted.
of set theory, where the ellipsis may be replaced by term-forming operations such as a symbol for the powerset operation. There are two bounded quantifiers: 
and 
. These quantifiers bind the set variable x and contain a term t which may not mention x but which may have other free variables.
The semantics of these quantifiers is determined by the following rules:
A formula of set theory which contains only bounded quantifiers is called Δ0.
Bounded quantifiers are important in Kripke-Platek set theory and constructive set theory
, where only Δ0 separation
is included. That is, it includes separation for formulas with only bounded quantifiers, but not separation for other formulas. In KP the motivation is the fact that whether a set x satisfies a bounded quantifier formula only depends on the collection of sets that are close in rank to x (as the powerset operation can only be applied finitely many times to form a term). In constructive set theory, it is motivated on predicative grounds.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, bounded quantifiers are often added to a language in addition to the standard quantifiers "∀" and "∃". Bounded quantifiers differ from "∀" and "∃" in that bounded quantifiers restrict the range of the quantified variable. The study of bounded quantifiers is motivated by the fact that determining whether a sentence
Sentence (mathematical logic)
In mathematical logic, a sentence of a predicate logic is a boolean-valued well formed formula with no free variables. A sentence can be viewed as expressing a proposition, something that may be true or false...
with only bounded quantifiers is true is often not as difficult as determining whether an arbitrary sentence is true.
Common examples include "∀x>0", "∃y<0", "∀x ∊ ℝ". Informally "∀x>0" says "for all x where x is larger than 0", "∃y<0" says "there exists a y where y is less than 0" and "∀x ∊ ℝ" says "for all x where x is a real number". For example, "∀x>0 ∃y<0 (x = y2)" says "every positive number is the square of a negative number".
Bounded quantifiers in arithmetic
Suppose that L is the language of Peano arithmetic (the language of second-order arithmeticSecond-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. It was introduced by David Hilbert and Paul Bernays in their...
or arithmetic in all finite types would work as well). There are two types of bounded quantifiers:
and .These quantifiers bind the number variable n and contain a numeric term t which may not mention n but which may have other free variables. (By "numeric terms" here we mean terms such as "1 + 1", "2", "2 × 3", "m + 3", etc.)
These quantifiers are defined by the following rules (
denotes formulas):There are several motivations for these quantifiers.
- In applications of the language to recursion theoryRecursion theoryComputability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...
, such as the arithmetical hierarchyArithmetical hierarchyIn mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene-Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them...
, bounded quantifiers add no complexity. If
is a decidable predicate then 
and 
are decidable as well. - In applications to the study of Peano Arithmetic, formulas are sometimes provable with bounded quantifiers but unprovable with unbounded quantifiers.
For example, there is a definition of primality using only bounded quantifiers. A number n is prime if and only if there are not two numbers strictly less than n whose product is n. There is no quantifier-free definition of primality in the language
, however. The fact that there is a bounded quantifier formula defining primality shows that the primality of each number can be computably decided.In general, a relation on natural numbers is definable by a bounded formula if and only if it is computable in the linear-time hierarchy, which is defined similarly to the polynomial hierarchy
Polynomial hierarchy
In computational complexity theory, the polynomial hierarchy is a hierarchy of complexity classes that generalize the classes P, NP and co-NP to oracle machines...
, but with linear time bounds instead of polynomial. Consequently, all predicates definable by a bounded formula are Kalmár elementary, context-sensitive
Context-sensitive grammar
A context-sensitive grammar is a formal grammar in which the left-hand sides and right-hand sides of any production rules may be surrounded by a context of terminal and nonterminal symbols...
, and primitive recursive.
In the arithmetical hierarchy
Arithmetical hierarchy
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene-Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them...
, an arithmetical formula which contains only bounded quantifiers is called
, , and . The superscript 0 is sometimes omitted.Bounded quantifiers in set theory
Suppose that L is the language of set theory, where the ellipsis may be replaced by term-forming operations such as a symbol for the powerset operation. There are two bounded quantifiers: and . These quantifiers bind the set variable x and contain a term t which may not mention x but which may have other free variables.The semantics of these quantifiers is determined by the following rules:
A formula of set theory which contains only bounded quantifiers is called Δ0.
Bounded quantifiers are important in Kripke-Platek set theory and constructive set theory
Constructive set theory
Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. That is, it uses the usual first-order language of classical set theory, and although of course the logic is constructive, there is no explicit use of constructive types...
, where only Δ0 separation
Axiom schema of predicative separation
In axiomatic set theory, the axiom schema of predicative separation, or of restricted, or Δ0 separation, is a schema of axioms which is a restriction of the usual axiom schema of separation in Zermelo-Fraenkel set theory. It only asserts the existence of a subset of a set if that subset can...
is included. That is, it includes separation for formulas with only bounded quantifiers, but not separation for other formulas. In KP the motivation is the fact that whether a set x satisfies a bounded quantifier formula only depends on the collection of sets that are close in rank to x (as the powerset operation can only be applied finitely many times to form a term). In constructive set theory, it is motivated on predicative grounds.
See also
- Subtyping — bounded quantification in type theoryType theoryIn mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
- System F<: — a polymorphicSystem FSystem F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
typed lambda calculusTyped lambda calculusA typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
with bounded quantification