Bounded quantifier


Bounded quantifier

In the study of formal theories in mathematical logic, bounded quantifiers are often added to a language. These are two quantifiers in addition to forall and exists. They are motivated by the fact that determining whether a sentence with only bounded quantifiers is true is not as difficult as determining whether an arbitrary sentence is true.

Bounded quantifiers in arithmetic

Suppose that "L" is the language of Peano arithmetic (the language of second-order arithmetic or arithmetic in all finite types would work as well). There are two bounded quantifiers: forall n < t and exists n < t.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.

The semantics of these quantifiers is determined by the following rules::exists n < t, phi Leftrightarrow exists n ( n < t land phi):forall n < t, phi Leftrightarrow forall n ( n < t ightarrow phi)

There are several motivations for these quantifiers.
* In applications of the language to recursion theory, such as the arithmetical hierarchy, bounded quantifiers add no complexity. If phi is a decidable predicate then exists n < t , phi and forall n < t, phi 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 quantifers. 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 langle 0,1,+, imes, <, = angle, 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 Sigma^0_0, Delta^0_0, and Pi^0_0. The superscript 0 is sometimes omitted.

Bounded quantifiers in set theory

Suppose that "L" is the language langle in, ldots, = angle 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: forall x in t and exists x in t. 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::exists x in t, phi Leftrightarrow exists x ( x in t land phi):forall x in t, phi Leftrightarrow forall x ( x in t ightarrow phi)

A formula of set theory which contains only bounded quantifiers is called &Delta;0.

Bounded quantifiers are important in Kripke-Platek set theory and constructive set theory, where only &Delta;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.

References

*
*


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • List of mathematics articles (B) — NOTOC B B spline B* algebra B* search algorithm B,C,K,W system BA model Ba space Babuška Lax Milgram theorem Baby Monster group Baby step giant step Babylonian mathematics Babylonian numerals Bach tensor Bach s algorithm Bachmann–Howard ordinal… …   Wikipedia

  • Arithmetical hierarchy — In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene hierarchy classifies certain sets based on the complexity of formulas that define them. Any set that receives a classification is called arithmetical. The… …   Wikipedia

  • Presburger arithmetic — is the first order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who published it in 1929. It is not as powerful as Peano arithmetic because it omits multiplication.OverviewThe language of Presburger… …   Wikipedia

  • Арифметика Пресбургера — Арифметика Пресбургера  это теория первого порядка описывающая натуральные числа со сложением, но в отличие от арифметики Пеано, исключающая высказывания относительно умножения. Названа в честь польского математика Мозеса Пресбургера,… …   Википедия

  • List of algebraic structures — In universal algebra, a branch of pure mathematics, an algebraic structure is a variety or quasivariety. Abstract algebra is primarily the study of algebraic structures and their properties. Some axiomatic formal systems that are neither… …   Wikipedia

  • Non-standard calculus — Abraham Robinson Contents 1 Motivation …   Wikipedia

  • Outline of algebraic structures — In universal algebra, a branch of pure mathematics, an algebraic structure is a variety or quasivariety. Abstract algebra is primarily the study of algebraic structures and their properties. Some axiomatic formal systems that are neither… …   Wikipedia

  • Uclid — (pronounced IPA|/ˈjuklɪd/, the same as Euclid ) is a decision procedure for CLU logic and can be used as a tool for bounded model checking of infinite state systems.Decision Procedure and Verification ToolUCLID is a tool for verifying models of… …   Wikipedia

  • Karp-Lipton theorem — The Karp–Lipton theorem in complexity theory states that if the boolean satisfiability problem (SAT) can be solved by Boolean circuits with a polynomial number of logic gates, then :Pi 2 , = Sigma 2 , and therefore mathrm{PH} , = Sigma 2 ,.That… …   Wikipedia

  • First-order logic — is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic (a less… …   Wikipedia