Bounded quantifier

From Wikipedia, the free encyclopedia

  (Redirected from Bounded quantifiers)

Jump to navigation Jump to search

This article is about bounded quantification in mathematical logic. For bounded quantification in type theory, see Bounded quantification.

In the study of formal theories in mathematical logic, bounded quantifiers are often included in a formal 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.

Contents

• 1 Examples
• 2 Bounded quantifiers in arithmetic
• 3 Bounded quantifiers in set theory
• 4 See also
• 5 References

Examples[edit]

Examples of bounded quantifiers in the context of real analysis include:

• ${\displaystyle \forall x>0}$ - for all x where x is larger than 0
• ${\displaystyle \exists y<0}$ - there exists a y where y is less than 0
• ${\displaystyle \forall x\in \mathbb {R} }$ - for all x where x is a real number
• ${\displaystyle \forall x>0\quad \exists y<0\quad (x=y^{2})}$ - every positive number is the square of a negative number

Bounded quantifiers in arithmetic[edit]

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 types of bounded quantifiers: ${\displaystyle \forall n<t}$ and ${\displaystyle \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. ("Numeric terms" here means terms such as "1 + 1", "2", "2 × 3", "m + 3", etc.)

These quantifiers are defined by the following rules (${\displaystyle \phi }$ denotes formulas):

${\displaystyle \exists n<t\,\phi \Leftrightarrow \exists n(n<t\land \phi )}$

${\displaystyle \forall n<t\,\phi \Leftrightarrow \forall n(n<t\rightarrow \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 ${\displaystyle \phi }$ is a decidable predicate then ${\displaystyle \exists n<t\,\phi }$ and ${\displaystyle \forall n<t\,\phi }$ are decidable as well.
• In applications to the study of Peano arithmetic, the fact that a particular set can be defined with only bounded quantifiers can have consequences for the computability of the set. 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 ${\displaystyle \langle 0,1,+,\times ,<,=\rangle }$, 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 that contains only bounded quantifiers is called ${\displaystyle \Sigma _{0}^{0}}$, ${\displaystyle \Delta _{0}^{0}}$, and ${\displaystyle \Pi _{0}^{0}}$. The superscript 0 is sometimes omitted.

Bounded quantifiers in set theory[edit]

Suppose that L is the language ${\displaystyle \langle \in ,\ldots ,=\rangle }$ of the Zermelo–Fraenkel 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: ${\displaystyle \forall x\in t}$ and ${\displaystyle \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:

${\displaystyle \exists x\in t\ (\phi )\Leftrightarrow \exists x(x\in t\land \phi )}$

${\displaystyle \forall x\in t\ (\phi )\Leftrightarrow \forall x(x\in t\rightarrow \phi )}$

A ZF formula that contains only bounded quantifiers is called ${\displaystyle \Sigma _{0}}$, ${\displaystyle \Delta _{0}}$, and ${\displaystyle \Pi _{0}}$. This forms the basis of the Lévy hierarchy, which is defined analogously with the arithmetical hierarchy.

Bounded quantifiers are important in Kripke–Platek set theory and constructive set theory, where only Δ₀ 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.

See also[edit]

• Subtyping — bounded quantification in type theory
• System F_<: — a polymorphic typed lambda calculus with bounded quantification

References[edit]

• Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.
• Kunen, K. (1980). Set theory: An introduction to independence proofs. Elsevier. ISBN 0-444-86839-9.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Bounded_quantifier&oldid=1045396848"

Categories:

• Quantification (science)
• Proof theory
• Computability theory

Navigation menu

Personal tools

• Not logged in
• Talk
• Contributions
• Create account
• Log in

Namespaces

• Article
• Talk

Variants expanded collapsed

Views

• Read
• Edit
• View history

More expanded collapsed

Search

Navigation

• Main page
• Contents
• Current events
• Random article
• About Wikipedia
• Contact us
• Donate

Contribute

• Help
• Learn to edit
• Community portal
• Recent changes
• Upload file

Tools

• What links here
• Related changes
• Upload file
• Special pages
• Permanent link
• Page information
• Cite this page
• Wikidata item

Print/export

• Download as PDF
• Printable version

Languages

• Português

Edit links

• This page was last edited on 20 September 2021, at 11:07 (UTC).
• Text is available under the Creative Commons Attribution-ShareAlike License; additional terms may apply. By using this site, you agree to the Terms of Use and Privacy Policy. Wikipedia® is a registered trademark of the Wikimedia Foundation, Inc., a non-profit organization.

• Privacy policy
• About Wikipedia
• Disclaimers
• Contact Wikipedia
• Mobile view
• Developers
• Statistics
• Cookie statement

• 
•