When are two proofs essentially the same? (2007)
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.