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

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!

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