nLab
quantification

Quantifiers

Idea

A quantifier is an operation in logic that moves a statement from one context to a related context.

Definitions

Quantification in first-order logic

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 n+1n + 1 types to a predicate on nn types.

Given a predicate PP on a type TT, the universal quantification of PP, denoted x:T,P(x)\forall\, x\colon T, P(x) (and with many variations in punctuation), is intended to be true if and only if P(a)P(a) is true for every possible element aa of TT. Similarly, the existential quantification of PP (also called its particular quantification), denoted x:T,P(x)\exists\, x\colon T, P(x), is intended to be true if and only if P(a)P(a) is true for at least one element aa of TT. However, it is quite possible that P(a)P(a) may be provable (in a given context Γ\Gamma) for every term aa of type TT that can actually be constructed (in Γ\Gamma), yet x:T,P(x)\forall\, x\colon T, P(x) cannot be proved; conversely, it is quite possible that x:T,P(x)\exists\, x\colon T, P(x) can be proved (in a given context) but P(a)P(a) cannot be proved for any term aa of type TT that can actually be constructed.

Therefore, we must define the quantifiers more carefully; one way to do this is as follows:

  • Q Γx:T,P(x)Q \vdash_{\Gamma}\forall\, x\colon T, P(x) if and only if Q Γ,x:TP(x)Q \vdash_{\Gamma, x\colon T} P(x);
  • x:T,P(x) ΓQ\exists\, x\colon T, P(x) \vdash_{\Gamma} Q if and only if P(x) Γ,x:TQP(x) \vdash_{\Gamma, x\colon T} Q.

Here, Γ\Gamma is an arbitrary context, and Γ,x:T\Gamma, x\colon T is that context supplemented by a free variable xx of type TT. Note that QQ is (a priori) a statement in the context Γ\Gamma but also needs to make sense in the context Γ,x:T\Gamma, x\colon T; 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 (\vdash), which is true for ordinary first-order logic.

From this definition, one can derive rules for the quantifiers in sequent calculus and natural deduction.

Quantification in first-order logic with equality

If all of our types have an equality predicate, then we can construct some fancier quantifiers.

Given a predicate PP on a type TT with equality, the uniqueness quantification of PP, denoted !x:T,P(x)\exists!\, x\colon T, P(x), may defined in terms of the universal and existential quantifiers as

!x:T,P(x)x:T,P(x)y:T,P(y)(x=y). \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 !x:T,P(x)\exists!\, x\colon T, P(x) is true iff P(a)P(a) is true for exactly one element aa of TT.

We can similarly write down quantifiers to say that PP 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.

Lawvere quantifiers: Quantification as adjunction

Given two contexts Γ\Gamma and Δ\Delta and an interpretation f:ΓΔf\colon \Gamma \to \Delta, we obtain an operation f *:Prop ΔProp Γf^*\colon Prop_\Delta \to Prop_\Gamma from the propositions in Δ\Delta to the propositions in Γ\Gamma. If this operation has a right adjoint, then this right adjoint is the universal quantifier along ff; if it has a left adjoint, then this is the existential quantifier along ff. The ordinary quantifiers in first-order logic are simply special cases of this where ff is given by weakening.

To bring this down to earth, let SS and TT be sets and let f:STf\colon S \to T 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 f *:𝒫T𝒫Sf^*\colon \mathcal{P}T \to \mathcal{P}S, the preimage map between power sets (often denoted f 1f^{-1}). Then the adjoints f\forall_f and f\exists_f are maps from 𝒫S𝒫T\mathcal{P}S \to \mathcal{P}T as follows:

  • fA{y:T|x:S,f(x)=yxA}\forall_f\, A \coloneqq \{ y\colon T \;|\; \forall\, x\colon S,\; f(x) = y \;\Rightarrow\; x \in A \};
  • fA{y:T|x:S,f(x)=yxA}\exists_f\, A \coloneqq \{ y\colon T \;|\; \exists\, x\colon S,\; f(x) = y \;\wedge\; x \in A \}.

Note that fA\exists_f A is simply the image of ff restricted to AA. Accordingly, one often denotes f\exists_f as f *f_* (if not simply ff). When using this notation, one can also denote f\forall_f as f !f_!.

When ff is the unique function from a set XX to the terminal set, 𝒫1\mathcal{P}1 is the two-element set and an object in 𝒫X\mathcal{P}X is a predicate on XX. The adjoints then map a predicate QQ to a truth value: * xX\exists x \in X such that Q(x)Q(x); * xX,Q(x).\forall x \in X, Q(x).

Guarded quantification: quantifying over subtypes

Recall that, given a type TT and a predicate QQ on TT, the subtype of TT defined by QQ is a type SS whose elements xx are thought of as elements of TT such that Q(x)Q(x) 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 TT, a predicate QQ on TT, and a predicate PP on TT, the guarded quantifications of PP relative to QQ are these propositions:

  • x:T,Q(x)P(x)\forall x\colon T, Q(x) \Rightarrow P(x),
  • x:T,Q(x)P(x)\exists x\colon T, Q(x) \wedge P(x).

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 QQ makes the type TT obvious, and especially when the variable appears only at beginning in this notation, it is quite common to suppress mention of TT and write Q(x),P(x)\forall Q(x), P(x) and Q(x),P(x)\exists Q(x), P(x). This is particularly common in untyped theories where TT would be suppressed anyway; for example, this is almost always how one writes guarded quantifiers in material set theory.

Bounded quantification: size issues and predicativity

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 Δ 0\Delta_0 consists of the formulas with only bounded quantifiers.

Internalised quantifiers

Heyting category

Categorified quantifiers

dependent productdependent sum

Examples

References

The identification of universal/existential quantification with adjoints of substitution/context extension (dependent product/dependent sum) originates around

  • Bill Lawvere, Adjointness in Foundations, (TAC), Dialectica 23 (1969), 281-296

  • Bill Lawvere Quantifiers and sheaves, Actes, Congrès intern, math., 1970. Tome 1, p. 329 à 334 (pdf)

Revised on December 5, 2012 00:04:32 by Urs Schreiber (131.174.40.191)