nLab universal quantifier

Idea

In logic, the universal quantifier “$\forall$” is the quantifier used to express, given a predicate $\phi$ with a free variable $x$ of type $T$, the proposition

$$\forall\, x\colon T, \phi x \,,$$

which is intended to be true if and only if $\phi a$ is true for every possible element $a$ of $T$.

Note that it is quite possible that $\phi a$ may be provable (in a given context) for every term $a$ of type $T$ that can actually be constructed in that context yet $\forall x\colon T, \phi x$ cannot be proved. Therefore, we cannot define the quantifier by taking the idea literally and applying it to terms.

Definition

We work in a logic in which we are concerned with which propositions entail which propositions (in a given context); in particular, two propositions which entail each other are considered equivalent.

Let $\Gamma$ be an arbitrary context and $T$ a type in $\Gamma$ so that $\Delta \coloneqq \Gamma, x\colon T$ is $\Gamma$ extended by a free variable $x$ of type $T$. We assume that we have a weakening rule that allows us to interpret any proposition $Q$ in $\Gamma$ as a proposition $Q[\hat{x}]$ in $\Delta$. Fix a proposition $P$ in $\Delta$, which we think of as a predicate in $\Gamma$ with the free variable $x$. Then the universal quantification of $P$ is any proposition $\forall\, x\colon T, P$ in $\Gamma$ such that, given any proposition $Q$ in $\Gamma$, we have

• $Q \vdash_{\Gamma}\forall\, x\colon T, P$ if and only if $Q[\hat{x}] \vdash_{\Gamma, x\colon T} P$.

It is then a theorem that the universal quantification of $P$, if it exists, is unique. The existence is typically asserted as an axiom in a particular logic, but this may be also be deduced from other principles (as in the topos-theoretic discussion below).

Often one makes the appearance of the free variable in $P$ explicit by thinking of $P$ as a propositional function and writing $P(x)$ instead; to go along with this one usually conflates $Q$ and $Q[\hat{x}]$. Then the rule appears as follows:

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

In terms of semantics (as for example topos-theoretic semantics; see the next section), the weakening from $Q$ to $Q[\hat{x}]$ corresponds to pulling back along a product projection $\sigma(T) \times A \to A$, where $\sigma(T)$ is the interpretation of the type $T$, and $A$ is the interpretation of $\Gamma$. In other words, if a statement $Q$ read in context $\Gamma$ is interpreted as a subobject of $A$, then the statement $Q$ read in context $\Delta = \Gamma, x \colon T$ is interpreted by pulling back along the projection, obtaining a subobject of $\sigma(T) \times A$.

As observed by Lawvere, we are not particularly constrained to product projections; we can pull back along any map $f \colon B \to A$. (Often we have a class of display maps and require $f$ to be one of these.) Alternatively, any pullback functor $f^\ast\colon Set/A \to Set/B$ can be construed as pulling back along an object $X = (f \colon B \to A)$, i.e., along the unique map $!\colon X \to 1$ corresponding to an object $X$ in the slice $Set/A$, since we have the identification $Set/B \simeq (Set/A)/X$.

In topos theory / in terms of adjunctions

In terms of the internal logic in some ambient topos $\mathcal{E}$,

• a type $X$ is given by an object $X \in \mathcal{E}$,

• the predicate $\phi$ is a (-1)-truncated object of the over-topos $\mathcal{E}/X$;

• a truth value is a (-1)-truncated object of $\mathcal{E}$ itself.

Universal quantification is essentially the restriction of the direct image right adjoint of a canonical étale geometric morphism $X_\ast$,

$$\mathcal{E}/X \stackrel{\overset{X_!}{\to}}{\stackrel{\overset{X^*}{\leftarrow}}{\underset{X_*}{\to}}} \mathcal{E} \,,$$

where $X^\ast$ is the functor that takes an object $A$ to the product projection $\pi \colon X \times A \to X$, where $X_! = \Sigma_X$ is the dependent sum (i.e., forgetful functor taking $f \colon A \to X$ to $A$) that is left adjoint to $X^\ast$, and where $X_\ast = \Pi_X$ is the dependent product operation that is right adjoint to $X^\ast$.

The dependent product operation restricts to propositions by pre- and postcomposition with the truncation adjunctions

$$\tau_{\leq -1} \mathcal{E} \stackrel{\overset{\tau_{\leq -1}}{\leftarrow}}{\underset{}{\hookrightarrow}} \mathcal{E}$$

to give universal quantification over the domain (or context) $X$:

$$\array{ \mathcal{E}/X & \stackrel{\overset{X_!}{\to}}{\stackrel{\overset{X^*}{\leftarrow}}{\underset{X_*}{\to}}} & \mathcal{E} \\ {}^\mathllap{\tau_{\leq_{-1}}}\downarrow \uparrow && {}^\mathllap{\tau_{\leq_{-1}}}\downarrow \uparrow \\ \tau_{\leq_{-1}} \mathcal{E}/X & \stackrel{\overset{\exists_X}{\to}}{\stackrel{\overset{}{\leftarrow}}{\underset{\forall_X}{\to}}} & \tau_{\leq_{-1}}\mathcal{E} } \,.$$

Dually, the extra left adjoint $\exists_X$, obtained from the dependent sum $X_!$ by pre- and post-composition with the truncation adjunctions, expresses the existential quantifier. (The situation with the universal quantifier is somewhat simpler than for the existential one, since the dependent product automatically preserves $(-1)$-truncated objects (= subterminal objects), whereas the dependent sum does not.)

The same makes sense, verbatim, also in the (∞,1)-logic of any (∞,1)-topos.

This interpretation of universal quantification as the right adjoint to context extension is also used in the notion of hyperdoctrine.

In dependent type theory

In dependent type theory, the universal quantifier is the dependent product type of a family of h-propositions:

Formation rules for the universal quantifier:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isProp}(B(x))}{\Gamma \vdash \forall (x:A).B(x) \; \mathrm{type}}$$

Introduction rules for the universal quantifier:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isProp}(B(x)) \quad \Gamma, x:A \vdash b(x):B(x)}{\Gamma \vdash \lambda(x:A).b(x):\forall (x:A).B(x)}$$

Elimination rules for the universal quantifier:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isProp}(B(x)) \quad \Gamma \vdash f:\forall (x:A).B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash f(a):B[a/x]}$$

Computation rules for the universal quantifier:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isProp}(B(x)) \quad \Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_\forall:\lambda(x:A).b(x)(a) =_{B[a/x]} b[a/x]}$$

Uniqueness rules for the universal quantifier:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isProp}(B(x)) \quad \Gamma \vdash f:\forall (x:A).B(x)}{\Gamma \vdash \eta_\forall:f =_{\forall (x:A).B(x)} \lambda(x).f(x)}$$

The dependent product type of a family of h-propositions is always an h-proposition.

One doesn’t need all dependent product types to define universal quantifiers. The isProp types are definable without all dependent product types, by use of center of contraction, which are also definable without all dependent product types. This means that one could define the type-theoretic internal logic of a Heyting category or Boolean category which are not locally cartesian closed, for strongly predicative mathematics.

Examples

Let $\mathcal{E} =$ Set, let $X = \mathbb{N}$ be the set of natural numbers and let $\phi \coloneqq 2\mathbb{N} \hookrightarrow \mathbb{N}$ be the subset of even natural numbers. This expresses the proposition $\phi(x) \coloneqq IsEven(x)$.

Then the dependent product

$$(\phi \in Set/{\mathbb{N}}) \mapsto (\prod_{x\colon X} \phi(x) \in Set)$$

is the set of sections of the bundle $2 \mathbb{N} \hookrightarrow \mathbb{N}$. But since over odd numbers the fiber of this bundle is the empty set, there is no possible value of such a section and hence the set of sections is itself the empty set, so the statement “all natural numbers are even” is, indeed, false.

Related concepts

• necessity, example

• existential quantifier

• generalized quantifier

$\phantom{-}$symbol$\phantom{-}$	$\phantom{-}$in logic$\phantom{-}$
$\phantom{A}$$\in$	$\phantom{A}$element relation
$\phantom{A}$$\,:$	$\phantom{A}$typing relation
$\phantom{A}$$=$	$\phantom{A}$equality
$\phantom{A}$$\vdash$$\phantom{A}$	$\phantom{A}$entailment / sequent$\phantom{A}$
$\phantom{A}$$\top$$\phantom{A}$	$\phantom{A}$true / top$\phantom{A}$
$\phantom{A}$$\bot$$\phantom{A}$	$\phantom{A}$false / bottom$\phantom{A}$
$\phantom{A}$$\Rightarrow$	$\phantom{A}$implication
$\phantom{A}$$\Leftrightarrow$	$\phantom{A}$logical equivalence
$\phantom{A}$$\not$	$\phantom{A}$negation
$\phantom{A}$$\neq$	$\phantom{A}$negation of equality / apartness$\phantom{A}$
$\phantom{A}$$\notin$	$\phantom{A}$negation of element relation $\phantom{A}$
$\phantom{A}$$\not \not$	$\phantom{A}$negation of negation$\phantom{A}$
$\phantom{A}$$\exists$	$\phantom{A}$existential quantification$\phantom{A}$
$\phantom{A}$$\forall$	$\phantom{A}$universal quantification$\phantom{A}$
$\phantom{A}$$\wedge$	$\phantom{A}$logical conjunction
$\phantom{A}$$\vee$	$\phantom{A}$logical disjunction
symbol	in type theory (propositions as types)
$\phantom{A}$$\to$	$\phantom{A}$function type (implication)
$\phantom{A}$$\times$	$\phantom{A}$product type (conjunction)
$\phantom{A}$$+$	$\phantom{A}$sum type (disjunction)
$\phantom{A}$$0$	$\phantom{A}$empty type (false)
$\phantom{A}$$1$	$\phantom{A}$unit type (true)
$\phantom{A}$$=$	$\phantom{A}$identity type (equality)
$\phantom{A}$$\simeq$	$\phantom{A}$equivalence of types (logical equivalence)
$\phantom{A}$$\sum$	$\phantom{A}$dependent sum type (existential quantifier)
$\phantom{A}$$\prod$	$\phantom{A}$dependent product type (universal quantifier)
symbol	in linear logic
$\phantom{A}$$\multimap$$\phantom{A}$	$\phantom{A}$linear implication$\phantom{A}$
$\phantom{A}$$\otimes$$\phantom{A}$	$\phantom{A}$multiplicative conjunction$\phantom{A}$
$\phantom{A}$$\oplus$$\phantom{A}$	$\phantom{A}$additive disjunction$\phantom{A}$
$\phantom{A}$$\&$$\phantom{A}$	$\phantom{A}$additive conjunction$\phantom{A}$
$\phantom{A}$$\invamp$$\phantom{A}$	$\phantom{A}$multiplicative disjunction$\phantom{A}$
$\phantom{A}$$\;!$$\phantom{A}$	$\phantom{A}$exponential conjunction$\phantom{A}$

References

The observation that substitution forms an adjoint pair/adjoint triple with the existential/universal quantifiers is due to

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

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

and further developed in

• William Lawvere, Equality in hyperdoctrines and

  comprehension schema as an adjoint functor_, Proceedings of the AMS Symposium on Pure Mathematics XVII (1970), 1-14.