Cryptomorphisms I am curious to collect examples of equivalent axiomatizations of mathematical structures.  The two examples that I have in mind are 


*

*Topological Spaces. These can be defined in terms of open sets, closed sets, neighbourhoods, the Kuratowski closure axioms, etc.

*Matroids.  These can be defined via independent sets, bases, circuits, rank functions, etc.
Are there are other good examples? 
Secondly, what are some advantages of multiple axiomatizations?
Obviously, one advantage is that one can work with the most convenient definition depending on the task at hand.  Another is that they allow different generalizations of the object in question.  For example, infinite matroids can be axiomatized by adapting the independent set axioms, but it is unknown how to axiomatize them via the circuit axioms.  An acceptable answer to the second question would be an example of a proof in one axiom system that doesn't translate easily (not sure how to make this precise) into another axiom system.  
 A: Here is one example that I always found fascinating.


*

*Frames are complete lattices which satisfy the infinite distributive law $$U \wedge \bigvee_{i \in I} V_i = \bigvee_{i \in I} U \wedge V_i.$$ In pointfree topology, these are used to abstract the lattice of open sets of a topological space.

*Complete Heyting algebras are complete lattices which have a binary operation ${\Rightarrow}$ that satisfies $$U \wedge V \leq W \quad\mbox{iff}\quad U \leq V \Rightarrow W.$$ These are primarily used to interpret intuitionistic logic.
The fact that these two types of lattices are cryptomorphic is essentially the Adjoint Functor Theorem (when viewing the underlying partial order as a category).
A: There are nice examples in geometry. For example, the Euclidean plane can
be characterized on the one hand by Hilbert's axioms, on the other hand by
axioms for complete ordered field $+$ vector space $+$ inner product. 
Another example is that of a Pappian plane, characterized on the one hand by 
the three projective plane axioms $+$ Pappus theorem, on the other hand by the 
field axioms (from which the plane may be constructed via homogeneous coordinates).
A: If you don't mind working in equational logic (no relation symbols besides equality, and focusing only on universally quantified equations), then there are many examples in universal algebra.  Groups have axiomatizations with and without a symbol for inverse, and even within the same language there is interest in alternative axiomatizations for the same theory, e.g. Boolean algebras, Heyting algebras, lattices.
If you want logics with more expressive power, you may consider interpretability results as well, which are ways of "encoding" one theory into another.  I only know of applications of this to show undecidability of theories, but there is a study of other objects around the notion of interpretability that Ralph McKenzie and others have created/discovered.
Gerhard "Ask Me About System Design" Paseman, 2010.02.18
A: A very familiar example is given by the different ways to express the completeness property of the real line --- Cauchy sequences converge, bounded nonempty sets have suprema, etc.  
A: The phenomenon that I think you have in mind has a name: cryptomorphism.  I learned the name from the writings of Gian-Carlo Rota; Rota's favorite example was indeed matroids.  Gerald Edgar informs me that the name is due to Garrett Birkhoff.
I think modern mathematics is replete with cryptomorphisms.  In my class today, I presented the "Omnibus Hensel's Lemma".  Part a) was: the following five conditions on a valued field are all equivalent.  Part b) was: complete fields satisfy these equivalent properties.  There are lots more equivalent conditions than the five I listed: see 
An unfamiliar (to me) form of Hensel's Lemma
and especially Franz Lemmermeyer's answer for further characterizations.  
I would say that the existence of cryptomorphisms is a sign of the richness and naturality of a mathematical concept -- it means that it has an existence which is independent of any particular way of thinking about it -- but that on the other hand the existence of not obviously equivalent cryptomorphisms tends to make things more complicated, not easier: you have to learn several different languages at once.  For instance, the origin of the question I cited above was the fact that in Tuesday's class I stpdly chose the wrong form of Hensel's Lemma to use to try to deduce yet another version of Hensel's Lemma: it didn't work!  Since we are finite, temporal beings, we often settle for learning only some of the languages, and this can make it harder for us to understand each other and also steer us away from problems that are more naturally phrased and attacked via the languages in which we are not fluent.  Some further examples:
I think that the first (i.e., most elementary) serious instance of cryptomorphism is the determinant.  Even the Laplace expansion definition of the determinant gives you something like $n$ double factorial different ways to compute it; the fact that these different computations are not obviously equivalent is certainly a source of consternation for linear algebra students.  To say nothing of the various different ways we want students to think about determinants.  It is "just" the signed change of volume of a linear transformation in Euclidean space (and the determinant over a general commutative ring can be reduced to this case).  And it is "just" the induced scaling factor on the top exterior power.  And it is "just" the unique scalar $\alpha(A)$ which makes the adjugate equation $A*\operatorname{adj}(A) = \alpha(A) I_n$ hold.  And so forth.  You have to be fairly mathematically sophisticated to understand all these things.
Other examples: 
Nets versus filters for convergence of topological spaces.  Most standard texts choose one and briefly allude to the other.  As G. Laison has pointed out, this is a disservice to students: if you want to do functional analysis (or read works by American mathematicians), you had better know about nets.  If you want to do topological algebra and/or logic (or read works by European mathematicians), you had better know about filters.
There are (at least) three axiomatizations of the concept of uniform space: (i) entourages, (ii) uniform covers, (iii) families of pseudometrics.  One could develop the full theory using just one, but at various points all three have their advantages.  Is there anyone who doesn't wish that there were just one definition that would work equally well in all cases?
A: Theodore Hailperin found a finite set of axioms for Quine's NF set theory. This finite axiomatization consists of a short list of particular instances of the NF axiom scheme of "stratefied comprehension." The advantage of Hailperin's alternate axiomatization is that it eliminates the necessity of referring to the concept of type in the definition of NF. See Hailperin's article "A set of axioms for logic" [Journal of Symbolic Logic, Volume 9, Issue 1 (1944), pp. 1-19].
A: For one take, see Feynman's lectures at Cornell.  Among other things, he talks about how there are many equivalent axiomatizations for physics.  Although the different axiomatizations are mathematically equivalent, they suggest different understandings of the world, and hence different experiments on the one hand and different metaphysics on the other.
A: Does the Cardinal Equivalence interest you?  Satisfying assignments have lower level semantics than valid quantifications, but their cardinalities are  equivalent: 
Boolean formulas:  |valid quantifications| = |satisfying assignments|. 
That is, for formula B(x1,..xn), variables ordered from 1 to n:  the number of valid quantification prefixes (q1..qn, over x1 to xn) of B, is Equivalent to the number of satisfying assignments of B.  The cardinality range is from zero for contradictions through 2^n for tautologies (technical notice:  n+1 bits are needed to represent these cardinality for tautologies; thus, there is some practical difficulty about finite propositional formulas performing logic with their own number of solutions). 
I only know this theorem for finite propositional boolean formulas; higher order extensions of the equivalence merely seem plausible, with some effort.  So, if you "axiomatize" counting propositional assignments, you would also be solving the higher level problem,  counting valid QBFs.  (Cardinal Equivalence is the only known equivalence in the boolean hierarchy; manifestations elsewhere seem "likely", but also "omh" (over my head).)
