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.
 A: 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!
A: What you're asking is exactly one of the things addressed by reverse math.
