Meaning of the word "axiom"
One usually describes an axiom to be a proposition regarded as self-evidently true without proof.
Thus, axioms are propositions we assume to be true and we use them in an axiomatic theory as premises to infer conclusions, which are called "theorems" of this theory.
For example, we can use the Peano axioms to prove theorems of arithmetic.
This is one meaning of the word "axiom". But I recognized that the word "axiom" is also used in quite different contexts.
For example, a group is defined to be an algebraic structure consisting of a set $G$, an operation $G\times G\to G: (a, b)\mapsto ab$, an element $1\in G$ and a mapping $G\to G: a\mapsto a^{-1}$ such that the following conditions, the so-called group axioms, are satisfied:
$\forall a, b, c\in G.\ (ab)c=a(bc)$,
$\forall a\in G.\ 1a=a=a1$ and
- $\forall a\in G.\ aa^{-1}=1=a^{-1}a$.
Why are these conditions (that an algebraic structure has to satisfy to be called a group) called axioms? What have these conditions to do with the word "axiom" in the sense specified above? I am really asking about this modern use of the word "axiom" in mathematical jargon. It would be very interesting to see how the modern use of the word "axiom" historically developed from the original meaning.
Now, let me give more details why it appears to me that the word is being used in two different meanings:
As peter.petrov did, one can argue that group theory is about the conclusions one can draw from the group axioms just as arithmetic is about the conclusions one can draw from the Peano axioms. But in my opinion there is a big difference: while arithmetic is really about natural numbers, the successor operation, addition, multiplication and the "less than" relation, group theory is not just about group elements, the group operation, the identity element and the inverse function. Group theory is rather about models of the group axioms. Thus: The axioms of group theory are not the group axioms, the axioms of group theory are the axioms of set theory.
Theorems of arithmetic can be formalized as sentences over the signature (a. k. a. language) $\{0, s, +, \cdot\}$, while theorems of group theory cannot always be formalized as sentences over the signature $\{\cdot, 1, ^{-1}\}$. Let me give an example: A typical theorem of arithmetic is the case $n=4$ of Fermat's last theorem. It can be formalized as follows over the signature $\{0, s, +, \cdot\}$: $$\neg\exists x\exists y\exists z(x\not = 0\land y\not = 0\land z\not = 0\quad\land\quad x\cdot x\cdot x\cdot x + y\cdot y\cdot y\cdot y = z\cdot z\cdot z\cdot z).$$ A typical theorem of group theory is Lagrange's theorem which states that for any finite group G, the order of every subgroup H of G divides the order of G. I think that one cannot formalize this theorem as a sentence over the "group theoretic" signature $\{\cdot, 1, ^{-1}\}$; or can one?
Axioms
Originally, "axioms" meant "self-evident truths", or at least what seemed self-evident. But the more important question is what axioms are used for. From the beginning, logic in some form has been an essential part of reasoning, and we reason about things all the time. Then whenever we want to convey our reasoning to other people, and want them to accept our viewpoint, we need to present a valid argument. What is a valid argument? It is a series of inferences or deductions, each one following from the previous ones logically. But no argument can get started without first making at least one assumption. If the other person accepts all our assumptions as well as all the deductive steps we take, they would also have to accept the conclusion of our argument.
The goal in convincing another person, therefore, is to make as few and as weak assumptions as we can in our argument. Sometimes, there are assumptions that the vast majority of people accept, in which case we could call them self-evident truths. This is a common source of the assumptions that we freely use in everyday argumentation.
But sometimes we do not want to bother ourselves with small details of the real world that might have to be catered to in self-evident truths. In this case, we often come up with idealized forms, that we still call axioms. The axioms that Euclid came up with to describe geometrical objects are of this kind. Although there are no physical manifestations of ideal lines (with zero thickness) and ideal points (with zero diameter) and ideal circles, what we can derive about ideal lines and points and circles is so general that the slight deviation of physical entities from these ideal objects does not affect the vast utility of the mathematical theorems about the ideal geometrical world. All we need to remember is that the ideal world is merely an approximation of the real world, and we can effectively apply the theorems (such as Pythagoras' theorem) to reality by taking those deviations into account.
Approximation is but the first step in from the real to the abstract. The objective of abstraction is to attempt to isolate the crucial structures from the not so important details or specific data. The next step is to consider worlds governed by different axioms (assumptions). A well-known historical example was the exploration of geometrical worlds that satisfy Euclid's axioms minus the parallel postulate. In that case, there are ways to interpret some of these worlds in a Euclidean world. But the point of laying down a collection of axioms describing a world is so that we can thereafter argue completely based on deductive reasoning without any appeal whatsoever to the intuitive nature of the axioms (whether or not they are)! This is the modern meaning of "axiom" in mathematics, more or less.
Algebraic structures
Now about your questions regarding the axiomatization of groups, first let us see what it really is about. The axioms for a group govern a single group, a world in which there is only one binary operation and it satisfies those properties as specified by the axioms. Inside any such world, you cannot tell whether it is finite or not, for example, not to say know the size of the world. Outside the world, however, you can, as long as your outside world is strong enough to talk about worlds that satisfy the group axioms!
In logic, a world satisfying a collection of axioms is called a model. Commonly, we work in a higher world that satisfies the axioms of ZFC, in which we can talk about sets of axioms and sets that are models for some set of axioms. That is precisely why we are able to prove Lagrange's theorem; we cannot express it as a statement over the language of group theory, as you noted, which intuitively you can understand to mean that if you are 'inside' any group you do not even have the ability to express the theorem, not to say prove it.
There are indeed many more theorems you can prove in ZFC about groups than you can simply by deduction using only the group axioms. This is a very common phenomenon in mathematics, where you need to work from 'outside' all algebraic structures of a certain family (such as fields) to do anything much. The reason is that the axioms governing the algebraic structure hold for every member of the family that satisfy those axioms, so naturally you are very limited in what you can prove using them.
As you remark, doing formal proofs from the group axioms is not very interesting -- that won't let us prove (or even formulate) most of the theorems of what we know as group theory.
So what does the group axioms have to do with axioms for general mathematical reasoning, such as the axioms of Peano Arithmetic or set theory? I would like to propose that the missing link is that model theory has interesting things to say about both kinds of axioms.
Model theory is mostly about relation between different models for the same set of axioms. In that it looks more like abstract algebra than proof theory does; doing model theory with the group axioms actually connects to what we view as group theory.
At the same time, useful results can come from applying model theory to the axioms of a proposed foundation for mathematics, such as ZFC. Model-theoretic results such as the Löwenheim-Skolem theorems are relevant all the time when we investigate the limits of what one can prove from those axioms.
In order to formulate model theory such that it applies to both of these situations, we need a word for "the conditions that define what is or isn't a model". The word "axiom" has been picked for that because in the case of a foundational theory those conditions are indeed supposed to be (at least somewhat close to) axioms in the traditional sense.
We then choose to use the same word for the conditions-for-being-a-model when we're talking about something less foundational such as groups. That's the beauty and curse of abstraction: It's often most powerful if we accept calling some thing by a name that originally only belonged to another thing else that it is merely formally analogous to.
In this way, what should perhaps by itself have been called the "group conditions" naturally become "group axioms" when we're using model-theoretic methods to study groups. And once that happens, it makes sense to reduce confusion by still calling them "axioms" when we're doing group theory with methods that are specific to groups.
(Repeat the above for all other kinds of algebraic structure, of course).
It happens that we find "interesting" to explore the conclusions that can be logically derived from a set of formal statements. It could be "interesting" for different reasons such as:
maybe the statements are all true for a specific "interesting" model (such as arithmetics or set theory) that we want to study
maybe the statements are all true for several structures that are not all necessarily interesting individually but are "widespread" in different areas of knowledge (such as groups/rings/ordered sets...)
Every time we want to explore the conclusions that follow from a set of statements we use to call them "axioms".