Universal Quantifier

Abstract

Universal quantification is a logical operation that asserts a property holds for all elements in a domain, written $\forall x.Px$. In type theory, universal quantification is interpreted as a dependent product type, providing a computational method to construct a proof for any element.

Definition

In Predicate Logic

In predicate logic, the universal quantifier $\forall$ binds a variable and asserts that a predicate holds for every element in the domain of discourse. The formula $\forall x\in A.Px$ is true if and only if $Pa$ holds for every element $a$ in $A$.

Under the Curry-Howard Correspondence, universal quantification corresponds to dependent function types. The constructive interpretation of $\forall x:A.Px$ is: $\Pi x:A.Px$ An element of this type is a function that takes any $x:A$ and produces a proof of $Px$.

In HoTT

In Homotopy Type Theory, the universal quantifier is defined as: $\forall x:A.Px:\equiv \Pi x:A.Px$

Unlike existential quantification, the universal quantifier is not truncated. The dependent product:

• Provides computational content via function application
• Allows extraction of proofs for specific elements
• Can be eliminated into arbitrary types
• Is not necessarily a proposition

When $Px$ is a proposition for all $x$, the dependent product $\Pi x:A.Px$ is also a proposition, making it equivalent to a truncated universal statement.

Type Rules

Introduction Rule

$\frac{\Gamma ,x:A⊢p:Px}{\Gamma ⊢(\lambda x.p):\Pi x:A.Px}$

To prove a universal statement, assume an arbitrary $x:A$ and construct a proof of $Px$. In type theory, this corresponds to lambda abstraction.

Elimination Rule

$\frac{\Gamma ⊢f:(\Pi x:A.Px)\Gamma ⊢a:A}{\Gamma ⊢fa:Pa}$

From a universal statement and a specific element $a:A$, obtain a proof of $Pa$ via function application.

Computation Rule

$(\lambda x.p)a\equiv p[x:=a]$

Function application computes by substituting the argument for the bound variable. This is beta reduction.

Eta Rule

For any $f:\Pi x:A.Px$: $f\equiv \lambda x.fx$

Every function is equal to its eta expansion.

Special Case: Implication

When $P$ does not depend on $x$, the dependent product reduces to ordinary function types: $\Pi x:A.P\equiv A\to P$

This shows that implication is a special case of universal quantification.

Duality with Existential Quantification

Universal quantification is dual to existential quantification: $\forall x.Px\equiv \neg \exists x.\neg Px$

In constructive logic, this duality requires the Law of the Excluded Middle.

Properties

Instantiation

Universal statements can be instantiated to any particular element: $\forall x.Px⊢Pa$

Distribution

Universal quantification distributes over conjunction: $\forall x.(Px\wedge Qx)\equiv (\forall x.Px)\wedge (\forall x.Qx)$

But not over disjunction in general.

Monotonicity

If $Px\to Qx$ for all $x$, then $(\forall x.Px)\to (\forall x.Qx)$.

Scope and Binding

The universal quantifier is a binding construct. In $\forall x:A.Px$, the variable $x$ is bound and its scope extends over $Px$.

Alpha-equivalent formulas are considered identical: $\forall x.Px\equiv \forall y.Py$

In Constructive Mathematics

In constructive mathematics, a proof of $\forall x.Px$ must provide a method to construct a proof of $Px$ for arbitrary $x$. The proof must be algorithmic.

BHK Interpretation

The BHK Interpretation views a proof of $\forall x\in S.Px$ as a function mapping each $x\in S$ to a proof of $Px$. This corresponds directly to the dependent product type.

In Different Logics

Classical Logic

In classical logic, universal quantification combined with negation gives full expressive power through duality with existential quantification.

Intuitionistic Logic

In intuitionistic logic, $\forall x.Px$ requires a constructive method to prove $Px$ for arbitrary $x$. The proof must be algorithmic.

Higher-Order Logic

In higher-order logic, universal quantification can range over predicates and functions, not just individuals.

Related Concepts

• Dependent Product: The type-theoretic counterpart
• Existential: The dual quantifier
• Lambda Calculus: The computational interpretation
• Function Type: The non-dependent special case
• Type Family: Dependent types in the codomain
• Predicate: What is quantified over
• BHK Interpretation: Constructive semantics
• Curry-Howard Correspondence: Logic-computation connection
• Beta Reduction: Computation rule for functions