To what extent must a proof "go a certain way" There are a number of theorems which have a multitude of proofs, yet all the proofs seem to ultimately rely on the same fundamental ideas.  For example, I ran into this blog post recently where Terrence Tao notes that the Brouwer fixed point theorem is of this character.  To quote:

"This theorem has many proofs, most of which revolve (either explicitly or implicitly) around the notion of the degree of a continuous map $f: S^{n-1} \rightarrow S^{n-1}$ of the unit sphere..."

(There are a lot of theorems of algebraic topology which seem to go this way: There are many ways to prove something using algebraic topology, but you can't seem to prove it without the algebraic topology.)
(Another example is complex analysis: There are some integrals that can be evaluated using a variety of contours, but to evaluate them with purely real methods is very difficult.)
On the other hand, there are some theorems which seem to have many proofs which are very profoundly different.  A former professor of mine commented that the fundamental theorem of algebra was of this sort.  He wondered whether there was any sense in which the many proofs were "the same" via some sort of "homotopy of proofs".
My question is whether there is any sense in which these informal observations can be made precise: 


*

*Is there a meaningful sense in which a proof must use a certain idea?  

*Are there meaningful ways of saying that two proofs are "essentially the same" or "essentially different"?
I am aware that there is at least one affirmative answer to this question: Many theorems can be proven to rely on the axiom of choice.  Perhaps there is some similar way to differentiate other kinds of proofs?  I.e. if you can find a reduced set of axioms such that one proof makes sense but the other doesn't, then you can say that the proofs are essentially different.  I'm well beyond my sphere of knowledge here, but hopefully my idea is sufficiently clear.
EDIT: After posting this, I found this question on mathoverflow, which pretty much answers the question.  I'm still curious about the specific examples I mentioned above (Brouwer fixed point theorem, contour integrals, etc.), so commentary about those would be welcome. 
 A: This could be treated as a very long comment and not neccessarily as a pure answer!
Well, as far as proofs are concerned, in logic there is a notion of deduction which's formal definition has as follows:

Deduction: Let $\phi$ be a theorem of a set $\Gamma$. Then a deduction of $\phi$ from $\Gamma$ is a finite sequences of logical types $\langle a_1,\dots,a_n\rangle$such that $a_n=\phi$ and for every $k\leq n$ either:
  
  
*
  
*$a_k$ belongs to $\Gamma\cup\mathrm{A}$ or
  
*$a_k$ can be deducted from some previous types $a_i,a_j$, $i,j<k$ with one of the rules of inference (e.g. modus ponens).
  
  
  where $\mathrm{A}$ is a set of logical Axioms we have predefined.

Now, let us suppose that we have a theorem $\phi$ and two deductions ("proofs") of it, let $D_1=\langle a_1,\dots,a_n\rangle$ and $D_2=\langle b_1,\dots,b_m\rangle$. Then, we could possibly say that these two proofs are essentially different iff 
$$\boxed{a_i\neq b_j\text{ for every $a_i,b_j\in\Gamma$ with $i=1,2,\dots,n$ and $j=1,2,\dots,m$}}$$
In that way, two proofs that do not use the same theorems to prove theorem $\phi$ may be considered essentially different. 
However, there could be more efficient ways of defining essential difference of proofs I can't think of right now...
Hope this added something useful! :)
A: This is a deep question. In practice, my criterion for when two proofs are "essentially the same" or not is whether they generalize in the same way. For example, in this blog post I give five proofs that the Euler characteristic of a closed orientable surface is even, which I would argue are all different because they generalize differently (actually that was the motivation for writing the post): 


*

*Proof 1 uses Poincare duality to show that the Euler characteristic of a closed orientable manifold which is a boundary is even. 

*Proof 2 uses Poincare duality, but in a different way, to show that the middle Betti number of a closed orientable manifold of dimension $2 \bmod 4$ is even. Unlike Proof 1, it uses the fact that in dimension $2 \bmod 4$ Poincare duality gives the middle cohomology a symplectic structure. 

*Proof 3 uses characteristic classes to show that the Stiefel-Whitney class $w_2$ vanishes. This is yet another application of Poincare duality. Essentially the same computation shows that $w_2$ also vanishes on closed orientable $3$-manifolds, which is no longer a statement about their Euler characteristic.

*Proof 4 uses the fact that closed orientable surfaces admit complex structures making them compact Kahler manifolds whose cohomologies admit Hodge decompositions. This is a genuinely different proof from the others since on the one hand it only generalizes to other compact Kahler manifolds and on the other hand it proves a stronger statement about them (that all of their odd Betti numbers are even). 

*Proof 5 again uses the fact that closed orientable surfaces admit complex structures, and applies the Hirzebruch-Riemann-Roch theorem. This is again a characteristic class computation as in Proof 3, but applied to Chern classes rather than Stiefel-Whitney classes. In the next complex dimension this argument generalizes to Noether's formula, which none of the other proofs can touch. 


Of course the "zeroth proof" is just computing the Betti numbers and seeing that they are equal to $1, 2g, 1$, but the question is whether there was an a priori reason the middle Betti number had to end up being even. Each proof gives a different reason (I would argue), although they're certainly related. 
A: As Qiaochu Yuan says at the beginning of his response, this is a deep question -- he then gives a very sophisticated set of examples where we have interestingly different proofs motivated by rather different ideas (which generalize differently).
It might help though also to have some much simpler examples of the same phenomenon (for the conceptual issues about sameness/difference/equivalence of proof-ideas arise even in simple cases). And the simplest interesting example I know is the case of different proofs that there are an infinite number of primes.
In the first chapter of their famous, wonderfully accessible, Proofs from the Book, Aigner and Ziegler offer no less than six proofs of this classical result, starting with Euclid's and including later proofs using analysis or topology. I can't improve on their exposition here, and it's just four pages. Look it up: a lovely example to think about -- especially as, in this case, it certainly doesn't seem that "all the proofs seem to ultimately rely on the same fundamental ideas", even on reflection. 
