When are two proofs essentially the same? (2007)
When two mathematical proofs reach the same conclusion, are they essentially the same object or meaningfully different? Commenters explore this through analogies with paths in space and with computer programs, drawing on ideas like Curry–Howard, constructive vs. classical logic, proof complexity and ordinal analysis to argue that proofs can differ in strength, structure, generality, and the additional information they convey. Several perspectives emerge: one views all correct proofs as reducible to a single underlying logical chain, while others maintain that the route taken — the tools, assumptions, and conceptual insights involved — is as important as the theorem proved, and resists any universal notion of proof equivalence.
What does it mean for two proofs to be “the same”?
- One camp argues that any two correct proofs of the same statement are “the same” at a deep logical level: they encode the same underlying facts once fully unraveled.
- Others push back: sameness of conclusion is trivial; what matters is structure, tools used, and what extra information the proof carries.
- Several comments stress that the notion of “same proof” depends heavily on how “same” is defined, and that both extremes (“every wording change differs” vs. “all proofs of X are identical”) are unhelpful.
Examples and counterexamples
- Classic examples are given for:
- Irrationality of √2 via continued fractions vs. prime factorization.
- Sum of first N integers via pairing vs. induction.
- Triangle angle sum and counting odd numbers up to a bound.
- Many argue these are clearly different proofs because they use distinct ideas and generalize differently.
- Path/geometry analogies (homotopy, different routes to a store with or without obstacles) are used to show that multiple proofs can encode different structural information beyond mere reachability.
Logic, type theory, and constructive content
- Curry–Howard / propositions-as-types: proofs correspond to programs; different programs of the same type suggest different proofs.
- Disagreement over whether we should “quotient” proofs so that only the proposition (type) matters, or keep multiple inhabitants (proofs) distinct.
- Classical vs. constructive logic raises a strong distinction: proofs by contradiction vs. constructive proofs can have very different informational content (e.g., exhibiting a witness vs. only showing existence).
Strength, levels, and generality of proofs
- Ordinal analysis and proof-theoretic strength are mentioned: two proofs of the same theorem, but in theories with different ordinals, can be seen as occurring at different “levels.”
- A proof that uses fewer or weaker assumptions, or generalizes to a broader result, is often treated as fundamentally different and “stronger.”
Program equivalence analogies and formal approaches
- Many comments lean on program equivalence: same input–output vs. same algorithm vs. structural bisimulation.
- Suggestions include using distances on formal proofs, proof nets, or transformations between proofs, but it’s widely acknowledged that making a rigorous, generally accepted metric of “proof sameness” is hard and largely unresolved.