What significance is there if a theorem can be proved in the same system in more than one way?

Question

Doesn't that imply some sort of redundancy or point to some inner connection between the axioms? Or is it the case that when all theorems used in the proofs are broken down to their axioms that the two proofs must in fact be equivalent?

Answer 1

Some proofs are of a very different style from others; geometrical vs algebraic vs formal vs generalized, etc. Technically everything known in mathematics can be proven from the axioms; that doesn't mean those theorems are all superfluous. One gauge of a mathematician's breadth of knowledge is how many totally different proofs of the Pythagorean theorem they know. (I still only know two). Mathematics is highly interconnected; we usually have several ways to say the same thing, and it is often much easier to prove something one way than another. That is the whole reason different coordinate systems exist, for example. We can write down the axioms in a small space; but the endless consequences of those axioms, and the chains of thought to get there, are interwoven and form a rich structure.

Answer 2

Complementary to Robert's answer, you might like to be aware of the proofs-as-programs or propositions-as-types paradigm, also known as the Curry-Howard correspondence. Under this correspondence, a logical statement (such as $\alpha \to (\beta \to \alpha)$) corresponds to a program (or function) that represents a proof of that statement (such as $x \mapsto y \mapsto x$ or $\lambda x \cdot \lambda y\cdot x$, if you prefer $\lambda$-notation). Under the Curry-Howard correspondence, the existence of multiple proofs of the same statement has very interesting consequences. For example, the proofs of the statement $(\alpha \to \alpha) \to (\alpha \to \alpha)$ provide a model for the natural numbers (the Church numerals).