Existential

Abstract

Existential quantification is a logical operation that asserts the existence of at least one element satisfying a given predicate, written $\exists x.Px$. In type theory, existential quantification is interpreted as the propositional truncation of a dependent sum, ensuring the witness cannot be computationally extracted.

Definition

In Predicate Logic

In predicate logic, the existential quantifier $\exists$ asserts existence without necessarily providing a witness. The formula $\exists x\in A.P(x)$ is true if at least one element of $A$ satisfies the predicate $P$.

Under the Curry-Howard Correspondence, existential quantification corresponds to dependent sum types. The constructive interpretation of $\exists x:A.P(x)$ is: $\Sigma x:A.Px$ An element of this type is a pair $(a,p)$ where $a:A$ is the witness and $p:Pa$ is the proof.

In HoTT

In Homotopy Type Theory, the existential quantifier is defined as: $\exists x:A.Px:\equiv \Vert \Sigma x:A.Px\Vert$

This is the $(-1)$-truncation of the dependent sum type $\Sigma x:A.Px$. The truncation ensures that:

• The type is a proposition (proof-irrelevant)
• No computational access to the specific witness is provided
• Any two proofs of $\exists x:A.Px$ are equal

This differs from the bare dependent sum $\Sigma x:A.Px$, which retains the witness and elimination rules allows extraction of that witness.

Type Rules

Introduction Rule

$\frac{\Gamma ⊢a:A\Gamma ⊢p:Pa}{\Gamma ⊢|a,p|:\exists x:A.Px}$

To prove an existential statement, provide a witness $a$ and a proof that $Pa$ holds. The notation $|a,p|$ indicates the pair is wrapped in the propositional truncation.

Elimination Rule

The elimination rule requires that the target type $Q$ is a proposition: $\frac{\Gamma ⊢e:\exists x:A.Px\Gamma ,x:A,p:Px⊢q:Q\text{isProp}(Q)}{\Gamma ⊢\text{elim}(e,\lambda x.\lambda p.q):Q}$

The function $\lambda x.\lambda p.q$ takes a witness $x:A$ and proof $p:Px$, but since $Q$ is a proposition, any two results are propositionally equal. This ensures the result is invariant over the choice of witness.

Computation Rule

$\text{elim}(|a,p|,f)\equiv fap$

This equality holds up to the path structure of the propositional truncation. In cubical settings, this may be a definitional equality.

Related Concepts

• Dependent Sum: The untruncated version with witness extraction
• Universal Quantifier: The dual quantifier
• Witness: An element satisfying the existential claim
• Truncation (HoTT): The operation that creates existentials
• Proposition (HoTT): The target type for elimination
• Axiom of Choice: Relates universal and existential quantifiers
• Type Family: The domain of quantification in type theory
• BHK Interpretation: Constructive semantics
• Proof Irrelevance: The key property of truncated existentials