In first-order logic, we have two basic quantifiers, each of which moves a predicate on one type to a proposition (a predicate on no types), or more generally moves a predicate on types to a predicate on types.
Given a predicate on a type , the universal quantification of , denoted (and with many variations in punctuation), is intended to be true if and only if is true for every possible element of . Similarly, the existential quantification of (also called its particular quantification), denoted , is intended to be true if and only if is true for at least one element of . However, it is quite possible that may be provable (in a given context ) for every term of type that can actually be constructed (in ), yet cannot be proved; conversely, it is quite possible that can be proved (in a given context) but cannot be proved for any term of type that can actually be constructed.
Therefore, we must define the quantifiers more carefully; one way to do this is as follows:
Here, is an arbitrary context, and is that context supplemented by a free variable of type . Note that is (a priori) a statement in the context but also needs to make sense in the context ; therefore, our logic needs an appropriate weakening rule for this to make sense. This definition also presumes that a statement (in any given context) can be identified precisely by placing it within the poset of statements (in that context) under entailment (), which is true for ordinary first-order logic.
If all of our types have an equality predicate, then we can construct some fancier quantifiers.
Given a predicate on a type with equality, the uniqueness quantification of , denoted , may defined in terms of the universal and existential quantifiers as
\exists!\, x\colon T, P(x) \;\equiv\; \exists\, x\colon T, P(x) \wedge \forall\, y\colon T, P(y) \Rightarrow (x = y) .
The intended interpretation is that is true iff is true for exactly one element of .
We can similarly write down quantifiers to say that holds for exactly two elements, at most three elements, at least four elements, etc. (These all require negation and therefore there are some slight variations possible when using intuitionistic logic.)
With these examples, one can see quite readily that quantification is about saying how often a statement is true, that is quantifying it.
Given two contexts and and an interpretation , we obtain an operation from the propositions in to the propositions in . If this operation has a right adjoint, then this right adjoint is the universal quantifier along ; if it has a left adjoint, then this is the existential quantifier along . The ordinary quantifiers in first-order logic are simply special cases of this where is given by weakening.
To bring this down to earth, let and be sets and let be a function. We will think of each set as defining a context with one free variable for an element of that set; then the propositions in one of those contexts correspond to the subsets of the corresponding set. In this way, we are looking at , the preimage map between power sets (often denoted ). Then the adjoints and are maps from as follows:
Note that is simply the image of restricted to . Accordingly, one often denotes as (if not simply ). When using this notation, one can also denote as .
When is the unique function from a set to the terminal set, is the two-element set and an object in is a predicate on . The adjoints then map a predicate to a truth value:
Recall that, given a type and a predicate on , the subtype? of defined by is a type whose elements are thought of as elements of such that holds. Many type theories do not include subtypes. However, we can mimic quantification over subtypes by using so-called ‘guarded’ quantifiers.
Specifically, given a type , a predicate on , and a predicate on , the guarded quantifications of relative to are these propositions:
We have already had an example of these on this page, in the discussion of the Lawvere quantifiers along a function.
When the notation for makes the type obvious, and especially when the variable appears only at beginning in this notation, it is quite common to suppress mention of and write and . This is particularly common in untyped theories where would be suppressed anyway; for example, this is almost always how one writes guarded quantifiers in material set theory.
When type theory is used as a foundation of mathematics, we have a freely generated universe of types (see also at type of types) and can also consider quantification over these. Similarly, when set theory is used as a foundation, we have a type of all sets and can consider quantification over this type. Such quantification is called unbounded and often forbidden in the axiom of separation (if it can be stated in the language at all), especially in predicative mathematics but also in some impredicative foundations, such as ETCS. Even if we allow unbounded quantification, if we wish to refer to large objects using the language of proper classes, this introduces the possibility of quantification over all classes, and this is forbidden even in ZFC and SEAR (although it is allowed in Morse–Kelley class theory).
In contrast, quantification over variables from small types (for a suitable notion of smallness) is called bounded quantification.
In the usual formulations of material set theory, there is only one type (the type of sets), which is not small. However, we can consider quantification over small subtypes using the trick of guarded quantification (above). So the axiom of separation in so-called ‘bounded’ variations of ZFC allows only statements in which all quantifiers are guarded by a set.
In classical mathematics, at least, formulas with unbounded quantifiers can be classified into the Lévy hierarchy, whose bottom level consists of the formulas with only bounded quantifiers.
… Heyting category …