Gian-Carlo Rota's famous 1991 essay, "The pernicious influence of mathematics upon philosophy" contains the following passage:
Perform the following thought experiment. Suppose that you are given two formal presentations of the same mathematical theory. The definitions of the first presentation are the theorems of the second, and vice versa. This situation frequently occurs in mathematics. Which of the two presentations makes the theory 'true'? Neither, evidently: what we have is two presentations of the same theory.
Rota's claim that "this situation frequently occurs in mathematics" sounds reasonable to me, because I feel that I have frequently encountered authors who, after proving a certain theorem, say something like, "This theorem can be taken to be the definition of X," with the implicit suggestion that the original definition of X would then become a theorem. However, when I tried to come up with explicit examples, I had a lot of trouble. My question is, does this situation described by Rota really arise frequently in the literature?
There is a close connection between this question and another MO question about cryptomorphisms. But I don't think the questions are exactly the same. For instance, different axiomatizations of matroids comprise standard examples of cryptomorphisms. It is true that one can take (say) the circuit axiomatization of a matroid and prove basis exchange as a theorem, or one can take basis exchange as an axiom and prove the circuit "axioms" as theorems. But these equivalences are all pretty easy to prove; in Oxley's book Matroid Theory, they all appear in the introductory chapter. As far as I know, none of the theorems in later chapters have the property that they could be taken as the starting point for matroid theory, with (say) basis exchange becoming a deep theorem. What I'm wondering is whether there are cases in which a significant piece of theory really is developed in two different ways in the literature, with a major theorem of Presentation A being taken as a starting point for Presentation B, and the definitions of Presentation A being major theorems of Presentation B.
Let me also mention that I don't think that reverse mathematics is quite what Rota is referring to. Brouwer's fixed-point theorem can be shown to imply the weak Kőnig's lemma over RCA0, but as far as I know, nobody seriously thinks that it makes sense to take Brouwer's fixed-point theorem as an axiom when developing the basics of analysis or topology.