Proof relevance

Proof relevance is the principle that proofs are not merely certificates of truth but mathematical objects worthy of study in their own right. In a proof-relevant system, two proofs of the same proposition are not automatically identified; they may differ in computational content, constructive information, or structural complexity. The Calculus of Constructions is proof-relevant by design: a proof of the existential proposition "there exists a prime greater than n" must contain the specific prime and the algorithm that verifies it, not merely a promise that such a prime exists.

Proof irrelevance — the alternative principle — treats all proofs of the same proposition as equal, collapsing the space of proofs to a single point. This is the default in classical set-theoretic semantics, where a proposition is either true or false and the manner of its verification is discarded. Proof irrelevance is computationally efficient but epistemically impoverished: it throws away the very information that makes constructive mathematics useful for programming.

The tension between proof relevance and proof irrelevance is one of the central design choices in modern type theory. Martin-Löf Type Theory is proof-relevant in its identity types, where the path between two equal terms carries geometric information. Homotopy Type Theory makes this explicit: proofs of equality are paths in a space, and different paths may be non-homotopic. The choice to make proofs relevant is not a philosophical luxury; it is the condition under which mathematics can be extracted as executable software.