Witness

Abstract

A witness is an element that satisfies an existential claim. In constructive mathematics and type theory, providing a witness is essential to proving existence.

Definition

Given a predicate $P:A\to \mathcal{U}$, a witness for the statement $\exists x:A.P(x)$ is an element $a:A$ such that $P(a)$ holds.

More formally, a witness is the first component of a proof of an existential statement. In the BHK Interpretation, a proof of $\exists x\in S.P(x)$ is a pair $(w,p)$ where:

• $w\in S$ is the witness
• $p$ is a proof that $P(w)$ holds

Constructive vs Classical

In Classical Logic

In classical logic, one can prove $\exists x.P(x)$ without exhibiting a specific witness. For example, using the Law of the Excluded Middle, one might prove existence by contradiction without constructing the element.

In Constructive Mathematics

In constructive mathematics, every existence proof must provide an explicit witness. This requirement ensures that proofs have computational content.

A famous example is the statement “there exist irrational numbers $a,b$ such that $a^b$ is rational.” The classical proof considers $x={\sqrt{2}}^{\sqrt{2}}$ and uses excluded middle, avoiding the need to determine which case holds. A constructive proof must exhibit specific values.

Type-Theoretic Perspective

In type theory, witnesses appear naturally in dependent sum types.

Dependent Sums

An element of $\Sigma x:A.P(x)$ is a pair $(a,p)$ where:

• $a:A$ is the witness
• $p:P(a)$ is the proof

The first projection ${\pi }_1:\Sigma x:A.P(x)\to A$ extracts the witness.

Propositional Truncation

In Homotopy Type Theory, propositional truncation $\Vert \Sigma x:A.P(x)\Vert$ asserts existence without providing computational access to the witness. This recovers the classical notion of existence while maintaining proof irrelevance.

The elimination principle for truncated types requires that the target type is a proposition, preventing extraction of the witness.

Examples

Mathematical Witnesses

• For $\exists n\in \mathbb{N}.n>10$, any natural number $n\ge 11$ is a witness
• For $\exists x\in \mathbb{R}.x^2=2$, both $\sqrt{2}$ and $-\sqrt{2}$ are witnesses
• For $\exists p\in \mathbb{N}.\text{prime}(p)\wedge p>100$, the number $101$ is a witness

Uniqueness

When a witness is unique, we write $\exists !x.P(x)$. In type theory, this is expressed as: $\Sigma x:A.P(x)\times \Pi y:A.P(y)\to x\equiv y$

The witness is unique up to equality.

Related Concepts

• Existential: The logical operation asserting existence
• Dependent Sum: The type-theoretic encoding
• Universal Quantifier: The dual quantifier
• Truncation (HoTT): Hiding witness information
• Axiom of Choice: Extracting witnesses from universal statements
• BHK Interpretation: Constructive semantics requiring witnesses
• Constructive Mathematics: Mathematics requiring explicit witnesses
• Proof Irrelevance: When the specific witness doesn’t matter