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?
Best Answer
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.