nLab
universal quantifier

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

In logic, the universal quantifier\forall” is the quantifier used to express, given a predicate ϕ\phi with a free variable xx of type TT, the proposition

x:T,ϕx, \forall\, x\colon T, \phi x \,,

which is intended to be true if and only if ϕa\phi a is true for every possible element aa of TT.

Note that it is quite possible that ϕa\phi a may be provable (in a given context) for every term aa of type TT that can actually be constructed in that context yet x:T,ϕx\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 TT a type in Γ\Gamma so that ΔΓ,x:T\Delta \coloneqq \Gamma, x\colon T is Γ\Gamma extended by a free variable xx of type TT. We assume that we have a weakening? principle that allows us to interpret any proposition QQ in Γ\Gamma as a proposition Q[x^]Q[\hat{x}] in Δ\Delta. Fix a proposition PP in Δ\Delta, which we think of as a predicate in Γ\Gamma with the free variable xx. Then the universal quantification of PP is any proposition x:T,P\forall\, x\colon T, P in Γ\Gamma such that, given any proposition QQ in Γ\Gamma, we have

  • Q Γx:T,PQ \vdash_{\Gamma}\forall\, x\colon T, P if and only if Q[x^] Γ,x:TPQ[\hat{x}] \vdash_{\Gamma, x\colon T} P.

It is then a theorem that the universal quantification of PP, 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 PP explicit by thinking of PP as a propositional function and writing P(x)P(x) instead; to go along with this one usually conflates QQ and Q[x^]Q[\hat{x}]. Then the rule appears 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).

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

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

In topos theory / in terms of adjunctions

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

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

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

where X *X^\ast is the functor that takes an object AA to the product projection π:X×AX\pi \colon X \times A \to X, where X !=Σ XX_! = \Sigma_X is the dependent sum (i.e., forgetful functor taking f:AXf \colon A \to X to AA) that is left adjoint to X *X^\ast, and where X *=Π XX_\ast = \Pi_X is the dependent product operation that is right adjoint to X *X^\ast.

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

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

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

/X X *X *X ! τ 1 τ 1 τ 1/X X X τ 1. \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 X\exists_X, obtained from the dependent sum X !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)(-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.

Examples

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

Then the dependent product

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

is the set of sections of the bundle 22 \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.

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 November 28, 2014 20:20:12 by Urs Schreiber (89.204.138.219)