nLab quantification

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

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

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

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

Here, $\Gamma$ is an arbitrary context, and $\Gamma, x\colon T$ is that context supplemented by a free variable $x$ of type $T$. Note that $Q$ is (a priori) a statement in the context $\Gamma$ but also needs to make sense in the context $\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 $P$ on a type $T$ with equality, the uniqueness quantifier of $P$, denoted $\exists!\, x\colon T, P(x)$, 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 $\exists!\, x\colon T, P(x)$ is true iff $P(a)$ is true for exactly one element $a$ of $T$.

Given a natural number $n$, we can similarly write down quantifiers to say that $P$ holds for exactly $n$ elements, at most $n$ elements, at least $n$ 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\colon \Gamma \to \Delta$, we obtain an operation $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 $f$; if it has a left adjoint, then this is the existential quantifier along $f$. The ordinary quantifiers in first-order logic are simply special cases of this where $f$ is given by weakening.

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

• $\forall_f\, A \coloneqq \{ y\colon T \;|\; \forall\, x\colon S,\; f(x) = y \;\Rightarrow\; x \in A \}$;

• $\exists_f\, A \coloneqq \{ y\colon T \;|\; \exists\, x\colon S,\; f(x) = y \;\wedge\; x \in A \}$.

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

When $f$ is the unique function from a set $X$ to the terminal set, $\mathcal{P}1$ is the two-element set and an object in $\mathcal{P}X$ is a predicate on $X$. The adjoints then map a predicate $Q$ to a truth value:

• $\exists x \in X$ such that $Q(x)$;

• $\forall x \in X, Q(x).$

Guarded quantification: quantifying over subtypes

Recall that, given a type $T$ and a predicate $Q$ on $T$, the subtype of $T$ defined by $Q$ is, or would be, a type $S$ whose elements (terms) $x$ are thought of as elements (terms) of $T$ such that $Q(x)$ holds. But many type theories do not include sub-type formation among their rules. However, we can mimic quantification over subtypes by using so-called ‘guarded’ quantifiers.

Specifically, given a type $T$, a predicate $Q$ on $T$, and a predicate $P$ on $T$, the guarded quantifications of $P$ relative to $Q$ are these propositions:

• $\underset{x\colon T}{\forall} \big( Q(x) \Rightarrow P(x) \big)$,

• $\underset{x\colon T}{\exists} \big( Q(x) \wedge P(x) \big)$.

We have already had an example of these on this page, in the discussion of the Lawvere quantifiers along a function (above).

When the notation for $Q$ makes the type $T$ obvious, and especially when the variable appears only at beginning in this notation, it is quite common to suppress mention of $T$ and write “$\forall Q(x), P(x)$” and “$\exists Q(x), P(x)$”. This is particularly common in untyped theories where the domain type “$T$” would be notationally 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 $\Delta_0$ consists of the formulas with only bounded quantifiers.

Internalised quantifiers

… Heyting category …

Categorified quantifiers

… dependent product … dependent sum …

Examples

• existential quantifier, dependent sum

• universal quantifier, dependent product

• uniqueness quantifier

Related concepts

• de dicto and de re

• Lévy hierarchy

• elimination of quantifiers

• generalized quantifier

References

General linguistical and philosophical discussion is in

• Quantifiers and quantification in Stanford Encyclopedia of Philosophy

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

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

  reprinted in: Reprints in Theory and Applications of Categories 16 (2006) 1-16 [tac:tr16, pdf]

• William Lawvere, Quantifiers and sheaves, Actes Congrès intern. Math. 1 (1970) 329-334 [pdf, pdf]

A definition of guarded and bounded quantification for the membership relation could be found in

• Michael Shulman (2018). Comparing material and structural set theories. arXiv:1808.05204.