nLab universal quantifier

Contents

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) 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 first-order logic, the universal quantifier\forall” is the quantifier used to express — given a predicate PP with a free variable tt of type TT — the proposition denoted

t:TP(t), \underset{ t \colon T } {\forall} P(t) \,,

which is meant to be true if and only if P(t)P(t) holds true for ALL possible elements tt of TT (all terms of type TT) — whence the notation “A” (even if upside-down) for this quantifier.

This notion is “dual” (in fact adjoint, see below) to the existential quantifier\exists” which asserts that P(t)P(t) holds true for some tt.

But beware that is quite possible that P(t)P(t) may be provable (in a given context) for every term tt of type TT that can actually be constructed in that context, and yet t:Tϕ(t) \underset{ t \colon T } {\forall} \phi(t) cannot be proved: The proper internal definition of universal quantification is as a right adjoint to context extension as brought out by the definition (1) below and expanded on further below.

Definition

We work in a logic in which we are concerned with which propositions entail which other propositions (in a given context); in particular, two propositions which entail each other are considered logically equivalent, denoted by “\Leftrightarrow”.

Let

so that

We assume that we have a weakening rule that allows us to interpret any proposition QQ in Γ\Gamma as

  • T *QT^\ast Q being a proposition in Δ\Delta.

Then for

its universal quantification is any proposition TP\underset{T}{\forall} P in Γ\Gamma such that, given any proposition QQ in Γ\Gamma, we have:

(1)Q ΓTPT *Q Γ,TP. Q \;\vdash_{\Gamma}\; \underset{ T }{\forall} \; P \;\;\;\;\;\;\; \Leftrightarrow \;\;\;\;\;\;\; T^\ast Q \;\vdash_{\Gamma, T}\; P \,.

It is then a theorem that 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(t)P(t) instead. Then the rule appears as follows:

Q Γt:TP(t)T *Q Γ,t:TP(t). Q \;\vdash_{\Gamma}\; \underset{ t \colon T }{\forall} P(t) \;\;\;\;\;\; \Leftrightarrow \;\;\;\;\;\; T^\ast Q \;\vdash_{\Gamma, t \colon T}\; P(t) \,.

In terms of semantics (as for example topos-theoretic semantics; see below), the context extension from QQ to T *QT^\ast Q 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 Δ=Γ,t:T\Delta = \Gamma, t \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 natural deduction the inference rules for the universal quantifier are given as

Γ,x:AP(x)propΓx:A.P(x)propΓ,x:AP(x)trueΓx:A.P(x)trueΓx:A.P(x)trueΓ,x:AP(x)true\frac{\Gamma, x:A \vdash P(x) \; \mathrm{prop}}{\Gamma \vdash \forall x:A.P(x) \; \mathrm{prop}} \qquad \frac{\Gamma, x:A \vdash P(x) \; \mathrm{true}}{\Gamma \vdash \forall x:A.P(x) \; \mathrm{true}} \qquad \frac{\Gamma \vdash \forall x:A.P(x) \; \mathrm{true}}{\Gamma, x:A \vdash P(x) \; \mathrm{true}}

Internal universal quantifier in set theory

In set theory, recall that a predicate on a set AA in the internal logic of set theory is represented by the preimage i *(a)i^*(a) of an injection i:BAi:B \hookrightarrow A. Because ii is an injection, each preimage i *(a)i^*(a) is a subsingleton for all aAa \in A, which represents the internal propositions of the set theory. The internal universal quantifier is represented by the Cartesian product of the family of sets (i *(a)) aA(i^*(a))_{a \in A}:

aA.i *(a) aAi *(a)\forall a \in A.i^*(a) \coloneqq \prod_{a \in A} i^*(a)

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.

In dependent type theory

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

(x:A).B(x)[ x:AB(x)]\forall (x:A).B(x) \coloneqq \left[\prod_{x:A} B(x)\right]

The axiom of function extensionality or weak function extensionality implies that 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.

Formation rules for the universal quantifier:

ΓAtypeΓ,x:AB(x)typeΓ,x:Ap(x):isProp(B(x))Γ(x:A).B(x)type\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:

ΓAtypeΓ,x:AB(x)typeΓ,x:Ap(x):isProp(B(x))Γ,x:Ab(x):B(x)Γλ(x:A).b(x):(x:A).B(x)\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:

ΓAtypeΓ,x:AB(x)typeΓ,x:Ap(x):isProp(B(x))Γf:(x:A).B(x)Γa:AΓf(a):B[a/x]\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:

ΓAtypeΓ,x:AB(x)typeΓ,x:Ap(x):isProp(B(x))Γ,x:Ab(x):B(x)Γa:AΓβ :λ(x:A).b(x)(a)= B[a/x]b[a/x]\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:

ΓAtypeΓ,x:AB(x)typeΓ,x:Ap(x):isProp(B(x))Γf:(x:A).B(x)Γη :f= (x:A).B(x)λ(x).f(x)\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)}

Closure of universal quantifiers under h-propositions rule:

ΓAtypeΓ,x:AB(x)typeΓ,x:Ap(x):isProp(B(x))Γweakfunext:isProp((x:A).B(x))\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 \mathrm{weakfunext}:\mathrm{isProp}(\forall (x:A).B(x))}

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=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 numbers. 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.

\phantom{-}symbol\phantom{-}\phantom{-}in logic\phantom{-}
A\phantom{A}\inA\phantom{A}element relation
A\phantom{A}:\,:A\phantom{A}typing relation
A\phantom{A}==A\phantom{A}equality
A\phantom{A}\vdashA\phantom{A}A\phantom{A}entailment / sequentA\phantom{A}
A\phantom{A}\topA\phantom{A}A\phantom{A}true / topA\phantom{A}
A\phantom{A}\botA\phantom{A}A\phantom{A}false / bottomA\phantom{A}
A\phantom{A}\RightarrowA\phantom{A}implication
A\phantom{A}\LeftrightarrowA\phantom{A}logical equivalence
A\phantom{A}¬\notA\phantom{A}negation
A\phantom{A}\neqA\phantom{A}negation of equality / apartnessA\phantom{A}
A\phantom{A}\notinA\phantom{A}negation of element relation A\phantom{A}
A\phantom{A}¬¬\not \notA\phantom{A}negation of negationA\phantom{A}
A\phantom{A}\existsA\phantom{A}existential quantificationA\phantom{A}
A\phantom{A}\forallA\phantom{A}universal quantificationA\phantom{A}
A\phantom{A}\wedgeA\phantom{A}logical conjunction
A\phantom{A}\veeA\phantom{A}logical disjunction
symbolin type theory (propositions as types)
A\phantom{A}\toA\phantom{A}function type (implication)
A\phantom{A}×\timesA\phantom{A}product type (conjunction)
A\phantom{A}++A\phantom{A}sum type (disjunction)
A\phantom{A}00A\phantom{A}empty type (false)
A\phantom{A}11A\phantom{A}unit type (true)
A\phantom{A}==A\phantom{A}identity type (equality)
A\phantom{A}\simeqA\phantom{A}equivalence of types (logical equivalence)
A\phantom{A}\sumA\phantom{A}dependent sum type (existential quantifier)
A\phantom{A}\prodA\phantom{A}dependent product type (universal quantifier)
symbolin linear logic
A\phantom{A}\multimapA\phantom{A}A\phantom{A}linear implicationA\phantom{A}
A\phantom{A}\otimesA\phantom{A}A\phantom{A}multiplicative conjunctionA\phantom{A}
A\phantom{A}\oplusA\phantom{A}A\phantom{A}additive disjunctionA\phantom{A}
A\phantom{A}&\&A\phantom{A}A\phantom{A}additive conjunctionA\phantom{A}
A\phantom{A}\invampA\phantom{A}A\phantom{A}multiplicative disjunctionA\phantom{A}
A\phantom{A}!\;!A\phantom{A}A\phantom{A}exponential conjunctionA\phantom{A}

References

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

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.

Last revised on November 13, 2023 at 13:48:39. See the history of this page for a list of all contributions to it.