Bounded quantifier

In the study of formal theories in mathematical logic, bounded quantifiers (a.k.a. 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 of bounded quantifiers in the context of real analysis include: for all x where x is larger than 0 there exists a y where y is less than 0 for all x where x is a real number every positive number is the square of a negative number 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: 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. ("Numeric terms" here means 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 theory, such as the arithmetical hierarchy, bounded quantifiers add no complexity. If is a decidable predicate then and 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 , however. The fact that there is a bounded quantifier formula defining primality shows that the primality of each number can be computably decided.