# Contents

## Idea

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

$\forall \phantom{\rule{thinmathspace}{0ex}}x:T,\varphi x\phantom{\rule{thinmathspace}{0ex}},$\forall\, x\colon T, \phi x \,,

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

Note that it is quite possible that $\varphi 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:T,\varphi 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 ≔\Gamma ,x:T$ is $\Gamma$ extended by a free variable $x$ of type $T$. We assume that we have a weakening? principle that allows us to interpret any proposition $Q$ in $\Gamma$ as a proposition $Q\left[\stackrel{^}{x}\right]$ 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 \phantom{\rule{thinmathspace}{0ex}}x:T,P$ in $\Gamma$ such that, given any proposition $Q$ in $\Gamma$, we have

• $Q{⊢}_{\Gamma }\forall \phantom{\rule{thinmathspace}{0ex}}x:T,P$ if and only if $Q\left[\stackrel{^}{x}\right]{⊢}_{\Gamma ,x: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\left(x\right)$ instead; to go along with this one usually conflates $Q$ and $Q\left[\stackrel{^}{x}\right]$. Then the rule appears as follows:

• $Q{⊢}_{\Gamma }\forall \phantom{\rule{thinmathspace}{0ex}}x:T,P\left(x\right)$ if and only if $Q{⊢}_{\Gamma ,x:T}P\left(x\right)$.

In terms of semantics (as for example topos-theoretic semantics; see the next section), the weakening from $Q$ to $Q\left[\stackrel{^}{x}\right]$ corresponds to pulling back along a product projection $\sigma \left(T\right)×A\to A$, where $\sigma \left(T\right)$ 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:T$ is interpreted by pulling back along the projection, obtaining a subobject of $\sigma \left(T\right)×A$.

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

## In topos theory / in terms of adjunctions

In terms of the internal logic in some ambient topos $ℰ$,

• a type $X$ is given by an object $X\in ℰ$,

• the predicate $\varphi$ is a (-1)-truncated object of the over-topos $ℰ/X$;

• a truth value is a (-1)-truncated object of $ℰ$ itself.

Universal quantification is essentially the restriction of the direct image right adjoint of a canonical étale geometric morphism ${X}_{*}$,

$ℰ/X\stackrel{\stackrel{{X}_{!}}{\to }}{\stackrel{\stackrel{{X}^{*}}{←}}{\underset{{X}_{*}}{\to }}}ℰ\phantom{\rule{thinmathspace}{0ex}},$\mathcal{E}/X \stackrel{\overset{X_!}{\to}}{\stackrel{\overset{X^*}{\leftarrow}}{\underset{X_*}{\to}}} \mathcal{E} \,,

where ${X}^{*}$ is the functor that takes an object $A$ to the product projection $\pi :X×A\to X$, where ${X}_{!}={\Sigma }_{X}$ is the dependent sum (i.e., forgetful functor taking $f:A\to X$ to $A$) that is left adjoint to ${X}^{*}$, and where ${X}_{*}={\Pi }_{X}$ is the dependent product operation that is right adjoint to ${X}^{*}$.

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

${\tau }_{\le -1}ℰ\stackrel{\stackrel{{\tau }_{\le -1}}{←}}{\underset{}{↪}}ℰ$\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$:

$\begin{array}{ccc}ℰ/X& \stackrel{\stackrel{{X}_{!}}{\to }}{\stackrel{\stackrel{{X}^{*}}{←}}{\underset{{X}_{*}}{\to }}}& ℰ\\ {}^{{\tau }_{{\le }_{-1}}}↓↑& & {}^{{\tau }_{{\le }_{-1}}}↓↑\\ {\tau }_{{\le }_{-1}}ℰ/X& \stackrel{\stackrel{{\exists }_{X}}{\to }}{\stackrel{\stackrel{}{←}}{\underset{{\forall }_{X}}{\to }}}& {\tau }_{{\le }_{-1}}ℰ\end{array}\phantom{\rule{thinmathspace}{0ex}}.$\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 $\left(-1\right)$-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.

## Examples

Let $ℰ=$ Set, let $X=ℕ$ be the set of natural numbers and let $\varphi ≔2ℕ↪ℕ$ be the subset of even natural numebrs. This expresses the proposition $\varphi \left(x\right)≔\mathrm{IsEven}\left(x\right)$.

Then the dependent product

$\left(\varphi \in \mathrm{Set}/ℕ\right)↦\left(\prod _{x:X}\varphi \left(x\right)\in \mathrm{Set}\right)$(\phi \in Set/{\mathbb{N}}) \mapsto (\prod_{x\colon X} \phi(x) \in Set)

is the set of sections of the bundle $2ℕ↪ℕ$. 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.

## References

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

• 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)

and further developed in

• Bill Lawvere, Equality in hyperdoctrines and comprehension schema as an adjoint functor, Proceedings of the AMS Symposium on Pure Mathematics XVII (1970), 1-14.

Revised on December 13, 2012 19:58:09 by David Corfield (129.12.18.29)