nLab existential 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 logic, the existential quantifier (or particular quantifier) “\exists” is a quantifier used to express, given a predicate ϕ\phi with a free variable xx of type TT, the proposition

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

which is intended to be true if and only if ϕa\phi a is true for at least one object aa of type TT.

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

Definition

In logic

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 rule 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 existential quantification of PP is any proposition x:T,P\exists\, x\colon T, P in Γ\Gamma such that, given any proposition QQ in Γ\Gamma, we have

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

It is then a theorem that the existential 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:

  • x:T,P(x) ΓQ\exists\, x\colon T, P(x) \vdash_{\Gamma} Q if and only if P(x) Γ,x:TQP(x) \vdash_{\Gamma, x\colon T} Q.

In natural deduction the inference rules for the existential quantifier are given as

Γ,x:AP(x)propΓx:A.P(x)prop\frac{\Gamma, x:A \vdash P(x) \; \mathrm{prop}}{\Gamma \vdash \exists x:A.P(x) \; \mathrm{prop}}
Γ,x:AP(x)propΓx:AΓP(x)trueΓx:A.P(x)true\frac{\Gamma, x:A \vdash P(x) \; \mathrm{prop} \quad \Gamma \vdash x:A \quad \Gamma \vdash P(x) \; \mathrm{true}}{\Gamma \vdash \exists x:A.P(x) \; \mathrm{true}}
Γ,x:AP(x)propΓ,x:A.P(x)trueQpropΓ,x:A,P(x)trueQtrueΓ,x:A.P(x)trueQtrue\frac{\Gamma, x:A \vdash P(x) \; \mathrm{prop} \quad \Gamma, \exists x:A.P(x) \; \mathrm{true} \vdash Q \; \mathrm{prop} \quad \Gamma, x:A, P(x) \; \mathrm{true} \vdash Q \; \mathrm{true}}{\Gamma, \exists x:A.P(x) \; \mathrm{true} \vdash Q \; \mathrm{true}}

In type theory

In type theory under the identification of propositions as types, the existential quantifier is given by the bracket type of the dependent sum type. Existential quantifier types in general could be regarded as a particular sort of higher inductive type. In Coq syntax:

Inductive existquant (T:Type) (P:T->Type) : Type :=
| exist : forall (x:T), P x -> existquant T P
| contr0 : forall (p q : existquant T P) p == q

If the dependent type theory has a type of propositions Prop\mathrm{Prop}, such as the one derived from a type universe UU - A:UisProp(A)\sum_{A:U} \mathrm{isProp}(A), then the existential quantification of the family of types B(x)B(x) indexed by x:Ax:A is defined as the dependent function type

x:A.B(x) P:Prop( x:AB(x)P)P\exists x:A.B(x) \equiv \prod_{P:\mathrm{Prop}} \left(\prod_{x:A} B(x) \to P\right) \to P

By weak function extensionality, the disjunction of two types is a proposition.

Theorem

The two definitions above are equivalent.

Proof

The propositional truncation of a type AA is equivalent to the following dependent product type

[A] P:Prop(AP)P[A] \equiv \prod_{P:\mathrm{Prop}} (A \to P) \to P

Substituting the dependent sum type x:AB(x)\sum_{x:A} B(x) for AA, we have

[ x:AB(x)] P:Prop(( x:AB(x))P)P\left[\sum_{x:A} B(x)\right] \simeq \prod_{P:\mathrm{Prop}} \left(\left(\sum_{x:A} B(x)\right) \to P\right) \to P

Given any type CC, there is an equivalence

(( x:AB(x))C)( x:AB(x)C)\left(\left(\sum_{x:A} B(x)\right) \to C\right) \simeq \left(\prod_{x:A} B(x) \to C\right)

and if ABA \simeq B, then (AC)(BC)(A \to C) \simeq (B \to C). In addition, for all type families x:AB(x)x:A \vdash B(x), and x:AC(x)x:A \vdash C(x), if there is a family of equivalences e: x:AB(x)C(x)e:\prod_{x:A} B(x) \simeq C(x), then there is an equivalence ( x:AB(x))( x:AC(x))\left(\prod_{x:A} B(x)\right) \simeq \left(\prod_{x:A} C(x)\right). All this taken together means that there are equivalences

[ x:AB(x)]( P:Prop(( x:AB(x))P)P)( P:Prop( x:AB(x)C))\left[\sum_{x:A} B(x)\right] \simeq \left(\prod_{P:\mathrm{Prop}} \left(\left(\sum_{x:A} B(x)\right) \to P\right) \to P\right) \simeq \left(\prod_{P:\mathrm{Prop}} \left(\prod_{x:A} B(x) \to C\right)\right)

Properties

Categorical semantics

The categorical semantics of existential quantification is given by the (-1)-truncation of the dependent sum-construction along the projection morphism that projects out the free variable over which the existental quantifier quantifies.

Notice that the categorical semantics of the context extension from QQ to Q[x^]Q[\hat{x}] corresponds to base change/pullback along the 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.

(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.

Therefore in terms of the internal logic of a suitable category \mathcal{E} (with sufficient pullbacks)

Existential quantification is essentially the restriction of the extra left adjoint of a canonical étale geometric morphism X *X_\ast,

(X !X *X *):/XX *X *X !, (X_!\dashv X^*\dashv 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 sum 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 existential quantification over the domain (or context) XX:

/X X *X *X ! τ 1 τ 1 τ 1/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}{\to}}{\stackrel{\overset{}{\leftarrow}}{\underset{\forall}{\to}}} & \tau_{\leq_{-1}} \mathcal{E} } \,.

In other words, we obtain the existential quantifier by applying the dependent sum, then (1)(-1)-truncating the result. This is equivalent to constructing the image as a subobject of the codomain.

Dually, the direct image functor \forall (dependent product) expresses the universal quantifier. (In this case, it is somewhat simpler, since the dependent product automatically preserves (1)(-1)-truncated objects; no additional truncation step is necessary.)

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

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

Frobenius reciprocity

The extential quantifier and context extension is related via Frobenius reciprocity: if ψ\psi does not have xx as a free variable then

x(ϕψ)( xϕ)ψ. \exists_x (\phi \wedge \psi) \Leftrightarrow (\exists_x \phi) \wedge \psi \,.

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 sum

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

is simply the set 2Set2 \mathbb{N} \in Set of even natural numbers. Since this is inhabited, its (-1)-truncation is therefore the singleton set, hence the truth value true. Indeed, there exists an even natural number!

Notice that before the (1)(-1)-truncation the operation remembers not just that there is an even number, but it remembers “all proofs that there is one”, namely every example of an even number.

\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 existantial/universal quantifiers is due to

and further developed to the notion of hyperdoctrines 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.

The definition of the existential quantifier in dependent type theory as the propositional truncation of the dependent sum type is found in:

And the existential quantifier defined from the type of propositions and dependent product types can be found in:

  • Madeleine Birchfield, Constructing coproduct types and boolean types from universes, MathOverflow (web)

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