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