Proof Relevance

Proof relevance is the principle, central to modern type theory and constructive mathematics, that proofs are not merely evidence for the truth of a proposition but are structured mathematical objects that carry computationally meaningful content. In a proof-relevant framework, two different proofs of the same proposition are genuinely distinct entities, distinguishable by their internal structure and extractable computational behavior.

This stands in sharp contrast to classical logic and traditional Mathematics, where proofs are treated as interchangeable. In classical logic, if P is true, there is simply a proof of P—one proof is as good as another, and the proof itself is merely a means to establish the truth value. In proof-relevant systems, a proof of ∀x.∃y.P(x,y) is not merely a certificate that for every x there exists a y; it is a function that, given any x, computes the corresponding y and a proof that P(x,y) holds. The proof is the algorithm.

The demand for proof relevance is what makes the Curry-Howard correspondence computationally useful rather than merely structurally elegant. In proof assistants like Coq and Agda, extracting a program from a proof is possible only because the proof carries the computational content that classical logic discards. A non-constructive existence proof, which merely shows that assuming non-existence leads to contradiction, yields no extractable program. It is proof-irrelevant in the most literal sense: the proof has no content to extract.

Proof relevance also matters for the foundations of formal verification. When a theorem prover certifies that a sorting algorithm always produces sorted output, the proof is not merely a guarantee of correctness. It is a data structure that can be inspected, transformed, and composed with other proofs. Proof-relevant type systems—particularly those with dependent types—allow the type of a function to encode its full behavioral specification, making the boundary between program and proof vanish entirely.

The insistence on proof relevance is not a technical preference. It is a metaphysical commitment: mathematical truth is not a Boolean value but a computational process. To know that something exists is to know how to build it—and the proof is the blueprint.