When are two proofs essentially the same? (2007)

I'm reminded of the Philosophy of Computer Science entry in the Stanford Encyclopedia of Philosophy [0], which briefly considers what it means for two programs to be identical.

"... it has been argued that there are cases in which it is not possible to determine whether two programs are the same without making reference to an external semantics. Sprevak (2010) proposes to consider two programs for addition which differ from the fact that one operates on Arabic, the other one on Roman numerals. The two programs compute the same function, namely addition, but this cannot always be established by inspecting the code with its subroutines; it must be determined by assigning content to the input/output strings"

"The problem can be tackled by fixing an identity criterion, namely a formal relation, that any two programs should entertain in order to be defined as identical. Angius and Primiero (2018) show how to use the process algebra relation of bisimulation between the two automata implemented by two programs under examination as such an identity criterion. Bisimulation allows to establish matching structural properties of programs implementing the same function, as well as providing weaker criteria for copies in terms of simulation."

(Of course, it isn't surprising that this would be relevant, because proofs and programs themselves are isomorphic).

This technique seems rather stricter than what Gowers has in mind, but it seems helpful as a baseline.

0. https://plato.stanford.edu/entries/computer-science/

Reducing two mathematical proofs to being 'essentially the same' just because they reach the same conclusion overlooks something crucial: each proof isn’t merely a path to a result but a unique expression of understanding. A proof has its own logical and conceptual structure, and that structure isn’t interchangeable without losing some of its inherent value. Comparing proofs shouldn’t just focus on a shared outcome: the path taken, the relationships it establishes, and the concepts it explores are as fundamental as the conclusion itself. Perhaps it’s time to view mathematics not just as calculation, but as a real act of knowledge that in its diversity deepens our grasp of reality

Well, if you define a proof system as a series of potential manipulations of a space of true statements, a given proof is a sequence of manipulations and states and thus a path in a sort-of-metric space. Two proofs could said to be similar if their paths are "close" in that sort-of-metric space. Of course, you're left with the question of how close is close and whether "close" means close at one intermediate point or many. Moreover, mathematicians often like proofs that are more "cohesive" than just sequences of manipulations. So the question with real world would probably be a matter of mathematical taste as well as objective measures.

One way to compare proofs is to consider whether they belong to the same "level" or not. Consider by analogy whether a particular Turing machine halts. You can look at the sequence of configurations of the Turing machine at each step. Since the evolution of the machine's configuration is deterministic, any configuration along a "halting path" ends up in the same final configuration (i.e., the first configuration in a halting state).

But that's too difficult in some cases. Most of the Goodstein sequences reach extraordinarily high values before coming back down. How can we prove they all eventually reach 0? Even at small values of n, the sequence length of G(n) requires something on the order of the Ackermann function to specify bounds. We can't inspect these sequences directly to prove whether they reach 0. Instead we create a "parallel" sequence to a Goodstein sequence. Then we prove there exists an algorithm that maps from each item in the parallel sequence to an item in the Goodstein sequence such that both sequences are well-ordered and decreasing. If the parallel sequence reaches 0, then so does the Goodstein sequence. You could think of this as one Turing machine computing the configurations of another Turing machine or perhaps one branch of a tree "cross-predicting" the items along another branch. You aren't just following the branch to its end. In this sense, the proof occurs at a higher "level".

This concept is known as ordinal analysis and one can consider the proof-theoretic ordinal of any theory T. If T_1 and T_2 both prove a specific theorem and have the same proof-theoretic ordinal, you could consider the two proofs to occur on the same "level". Interestingly, Peano Arithmetic can prove that any specific Goodstein sequence reaches 0 but not that all Goodstein sequences reach 0—this requires a more powerful formal system. So if you prove a specific sequence reaches 0 using the more powerful system, I would say that's a fundamentally different proof.

See Girard, The Blind Spot: Lectures on Logic (2011) for some attempts at tackling this question. (in particular, his "proof nets" attempt to have a canonical form, such that we can identify differently drawn concrete proof nets as representing the same abstract proof)

https://en.wikipedia.org/wiki/Proof_net

> Is it ever possible to give a completely compelling argument that two proofs are genuinely different?

I think in some cases, we can. Sometimes one of the proofs generalizes better than the other because it uses strictly fewer assumptions. It seems fair to say those would have to be inequivalent.

See: https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_prob...

https://mathoverflow.net/questions/3776/when-are-two-proofs-...

> For example, it is often possible to convert a standard inductive proof into a proof by contradiction

I would not consider those the same though, as one is constructive and the other is not.

I was working with a friend writing a paper about the Ship of Theseus, but my friend kept replacing all of my arguments.

If I were allowed a small philosophical leeway, I'd argue that two correct proofs are always the same. For sure they may contain different words or make use of different "abstractions", but it just seems to me that these abstractions should be equivalent if one were willing to unravel it all to a certain degree. Essentially, all proof is, is a statement that says "this is true" and no matter which language you use to say it, you are saying the same thing.

> A couple of years ago I spoke at a conference about mathematics that brought together philosophers, psychologists and mathematicians. The proceedings of the conference will appear fairly soon

Can we do better?