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.
EDIT: In another MO question, someone quoted Bott as referring to "the old French trick of turning a theorem into a definition". I'm not sure if Bott and Rota had exactly the same concept in mind, but it seems related.
Best Answer
From a conversation I had with Gian-Carlo Rota when I was undergraduate, I know that one simple but important example that he specifically had in mind was the calculus of vector fields (whether specifically in three dimensions or more generally). The gradient, divergence, and curl of differentiable fields on ${\mathbb R}^{3}$ can be defined as particular combinations of partial derivatives—in which case it is necessary to prove that they represent geometrical objects (meaning they transform correctly). Alternatively, it is possible to specific purely geometrical definitions of all three objects, in which case it is necessary to prove that, when applied to sufficiently smooth functions, the can be calculated entirely in terms of partial derivatives. Whichever way you like to approach the theory, it is possible to find textbooks that take your preferred starting point and do a good job of explaining vector calculus—even though the two approaches are, philosophically, quite different in terms of what they seem to assume about what, say, $\operatorname{grad} f$ "really means." Moreover, there are also plenty of important theorems that can be proven from either starting point, without proving the equivalence first.
Somebody else, in the course of that conversation, mentioned the logarithm as an even more basic example. There are actually many ways of initially defining the logarithm, and Calculus by James Stewart (or the first edition, at least) actually demonstrates explicitly that you can begin with the logarithm as the inverse of the exponential, or you can define $\ln x=\int_{1}^{x}(1/t)\,dt$ and eventually prove all the same things.