{{Short description|Logical quantification that ranges over a subset of the universe of discourse}} {{about|bounded quantification in mathematical logic|bounded quantification in type theory|Bounded quantification}} In the study of formal theories in mathematical logic, '''bounded quantifiers''' (also known as '''restricted 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.
==Examples== Examples of bounded quantifiers in the context of real analysis include:
* <math>\forall x > 0</math> - for all ''x'' where ''x'' is larger than 0 * <math>\exists y < 0</math> - there exists a ''y'' where ''y'' is less than 0 * <math>\forall x \isin \mathbb{R}</math> - for all ''x'' where ''x'' is a real number * <math>\forall x > 0 \quad \exists y < 0 \quad (x = y^2)</math> - 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 arithmetic or arithmetic in all finite types would work as well). There are two types of bounded quantifiers: <math>\forall n < t</math> and <math>\exists n < t</math>. These quantifiers bind the number variable ''n'' using a numeric term ''t'' not containing ''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 (<math>\phi</math> denotes formulas): :<math>\exists n < t\, \phi \Leftrightarrow \exists n ( n < t \land \phi)</math> :<math>\forall n < t\, \phi \Leftrightarrow \forall n ( n < t \rightarrow \phi)</math>
There are several motivations for these quantifiers. * In applications of the language to computability theory, such as the arithmetical hierarchy, bounded quantifiers add no complexity. If <math>\phi</math> is a decidable predicate then <math>\exists n < t \, \phi</math> and <math>\forall n < t\, \phi</math> 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 <math>\langle 0,1,+,\times, <, =\rangle</math>, 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 <math>\Sigma^0_0</math>, <math>\Delta^0_0</math>, and <math>\Pi^0_0</math>. The superscript 0 is sometimes omitted.
== Bounded quantifiers in set theory == Suppose that ''L'' is the language <math>\langle \in, \ldots, =\rangle</math> 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: <math>\forall x \in t</math> and <math>\exists x \in t</math>. 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: :<math>\exists x \in t\ (\phi) \Leftrightarrow \exists x ( x \in t \land \phi)</math> :<math>\forall x \in t\ (\phi) \Leftrightarrow \forall x ( x \in t \rightarrow \phi)</math>
A ZF formula that contains only bounded quantifiers is called <math>\Sigma_0</math>, <math>\Delta_0</math>, and <math>\Pi_0</math>. 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 Δ<sub>0</sub> 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 == * Subtyping — bounded quantification in type theory * System F<sub><:</sub> — a polymorphic typed lambda calculus with bounded quantification
== References == * {{cite book | author = Hinman, P. | title = Fundamentals of Mathematical Logic | publisher = A K Peters | year = 2005 | isbn = 1-56881-262-0}} * {{cite book | author= Kunen, K. |authorlink = Kenneth Kunen| title = Set theory: An introduction to independence proofs | url= https://archive.org/details/settheoryintrodu0000kune | url-access= registration | publisher = Elsevier | year = 1980 | isbn = 0-444-86839-9}}
Category:Quantifier (logic) Category:Proof theory Category:Computability theory