# Is it possible to formalize the relationship between different proofs of the same theorem?

Some theorems have many proofs. Examples include the Pythagorean Theorem and the Law of Quadratic Reciprocity. I was wondering if one could formalize the relationship between these proofs. Sure, they all eventually prove the theorem, but some may look more like one another while others may be very different, i.e. if the theorem is proved by means of different ideas. But after one has decided that two proofs are not the same, could we decide how much they differ from each other?

I think such a formalisation could be useful because I imagine it being used to create some kind of a "genealogy" of proofs. Such a genealogy could perhaps be visualised in some kind of a "tree of proofs". I suspect such a visualisation could deepen our understanding of mathematics.

-
The tools we have available are good at comparing syntax, but not good for semantics. In fact the whole idea of formalizing proofs is that you can get away with just looking at syntax. If you're talking about comparing the ideas underlying the proofs, rather than just the way they are expressed formally, I think that would be extremely difficult. – Robert Israel Sep 27 '11 at 15:52
See this and that entry of Gowers's blog. – Pierre-Yves Gaillard Sep 27 '11 at 15:57
@Mr. Gaillard: These links look interesting, thank you. Do you know where to find the Conference Proceedings Mr. Gowers mentions? To Mr. Israel: OK, do you think comparing different proofs in the way they are expressed formally is more feasible? Moreover, do you think it could be useful? – Max Muller Sep 27 '11 at 16:05
It's certainly possible to compare proofs in the way they are expressed formally: you could just take the Hamming distance between the strings they correspond to. That would be useless, however. A more sophisticated comparison might take into account renaming variables and various types of trivial rearrangements. That would make it more difficult to compute the metric. I can imagine metrics whose computation might end up being NP-complete. – Robert Israel Sep 27 '11 at 16:21
Dear Max: You're welcome. For the Proceedings, I have no idea, sorry. You might try to email him. [You should use @Robert and @Pierre-Yves to alert Robert or me. The syntax is "at" "start of the user's name", without spaces, e.g. for me: @Pierre, or @Pierre-Yves, or @Pierre-YvesGaillard (without space between s and G). (The capitalization doesn't matter.) Sorry for using myself as an example!] – Pierre-Yves Gaillard Sep 27 '11 at 16:33

Quinn is correct that you can use reverse mathematics to formalize the "idea" of a proof, but I'd add that this is not the usual interpretation or project of reverse mathematics.

To answer your question, you first need to identify the big tools, or theorems, you use in your proof. Next, you formalize those theorems inside second order arithmetic. The field of reverse mathematics seeks to identify when these theorems are equivalent. Here, two theorems A and B are equivalent if you can prove B from A and visa versa, over $RCA_0$. This simply means that the proof B from A can also use axioms from the base theory $RCA_0$, which roughly corresponds to "computable mathematics.''

Now, you can formalize the statement 'proof I and proof II are the same' as the statement 'the theorems used in proof I are equivalent to the theorems used in proof II.'

In the Wikipedia article, you'll see that most theorems of mathematics end up being equivalent to one of five subsystems, which are strictly increasing in strength. In other words, most proofs of a given theorem will either be equivalent, or one proof will be stronger than the other.

On the other hand, recent research has shown there is a much more complicated set of relationships between certain weak combinatorial theorems. See http://www.nd.edu/~ddzhafar/The_Zoo.html for a nice picture. In this context, you can end up with two, non-equivalent proofs of the same theorem, where neither proof is stronger than the other.

This phenomena shows up theorems 3 and 5 of a paper I've just submitted (available here). In this paper, I give two incomparable proofs of a principle (called $RKL$). One proof uses $WKL$, and one proof uses $SRT^2_2$. These two theorems are known to be incomparable.

I hope this helps!

-
This certainly helps Stephen, thank you! Do you have any ideas on why of all theorems, the combinatorial ones have the most interesting set of relationships amongst each other? – Max Muller Oct 1 '11 at 10:51
The Zoo is now here: math.berkeley.edu/~damir/The_Zoo.html – Quinn Culver Apr 18 '13 at 22:48

What you're asking is exactly one of the things addressed by reverse math.

-