How does one show a set of axioms is independent? (of each other?)
The set $\mathcal{A}$ of axioms is independent if none of the elements of $\mathcal{A}$ is a consequence of the others. More formally still, the condition is that for every $\varphi\in \mathcal{A}$, the sentence $\varphi$ is not a theorem of the theory with axiom set $\mathcal{A}\setminus\{\varphi\}$.
That means your first interpretation is correct. To show independence, it is enough to produce for every $\varphi$ a structure $M_{\varphi}$ in which all the axioms in $\mathcal{A}\setminus\{\varphi\}$ are true , but $\varphi$ fails. This is a semantic argument. One can also imagine syntactic arguments, but semantic arguments are the mathematically natural ones.
Let's try to summarize the already given answers but starting from the beginning.
Syntax
Usually we express things by using finite strings of symbols taken from a particular set. The way to formalize this idea is to define language as the set from which you pick these symbols.
Let ${\cal V}$ be a nonempty and large enough set. This will be the set of variables of the language.
Let $$\mathrm{BIN}=\{\vee,\wedge,\implies,\iff\}$$ the set of binary connectives.
Then we define the language $L$ as the set $$L:={\cal V}\cup \mathrm{BIN}\cup \{\neg\}\cup \{),(\}$$ where we agree that all the sets involved are pairwise disjoint. I think all this symbols are self explanatory. Its intended meaning is the usual.
From this language we can form words, for example if you take $A,B$ variables then $$A,\quad )B\neg,\quad (\neg A\vee B)$$ are words.
Intuitively, the words you would use to express something "useful" are called formulas. For example, perhaps we all agree that the second word in the example above is not a formula. To be precise, let ${\cal W}(L)$ the set of words of $L$. The set of formulas of $L$ is defined as the smallest subset $X$ of ${\cal W}(L)$ which satisfies:
- it contains ${\cal V}$
- if $F\in X$ then $\neg F\in X$
- if $F\in X$ and $G\in X$ then for all $\alpha\in\mathrm{BIN}$, $(F\mathbin{\alpha} G)\in X$
The set of formulas of the language $L$ is called ${\cal F}(L)$. There is an equivalent inductive way of define ${\cal F}(L)$.
Then you can try to decide when a given formula is "true" or "false". To do this you consider maps $\delta:{\cal V}\to \{0,1\}$ and then you extend it to a map $\bar{\delta}$ defined on ${\cal F}(L)$ in an inductive fashion. For example, once $\bar{\delta}$ is defined for some formulas $A,B$ then $$\bar{\delta}((A\wedge B))=\delta{A}\cdot\delta{B}$$ which intuitively says that the formula $(A\wedge B)$ is false whenever $A$ or $B$ is false.
In this way you can define tautologies among other things, and study relations between formulas and theories (here theory is just a set of formulas), for example you might want to say when two different formulas are essentially the same.
The study of all this stuff is called propositional calculus.
But math is quite more complicated so we need more to abstract it.
Let $\cal C$ a nonempty set, a first order language $L$ is a set $$\begin{align*} L &:={\cal V}\cup \{\forall,\exists\}\cup \mathrm{BIN}\cup \{\neg\}\cup \{),(\}\\ &\phantom{{}:=}\cup{\cal C}\cup \bigcup_{i=1}^\infty \cal{F}_i \cup \bigcup_{i=1}^\infty \cal{R}_i \end{align*}$$ where all the sets involved are pairwise disjoint and:
- for each $n\geq 1$ the elements of ${\cal F}_n$/${\cal R}_n$ are called $n$-ary function/relation symbols.
- the elements of $\cal C$ are called constant symbols.
- Notice that (if present) the symbol for equality $\simeq$ is an element of $\cal{R}_2$.
The elements in the first row above are called logical symbols since they are common to all first order languages. When you specify a first order language you must only say what the no-logical symbols are. For example, for the language of groups you need a constant symbol, say $e$, and a binary function symbol, say $\ast$. This language would be then $$L_G=\{e,\ast\}.$$
As before you can define "useful" words from this language, and you can define formulas. But here we must be more careful. First we must define terms which are variables, constants or "valid" combinations of those with function symbols. For example, with $L_G$, $$v_0*v_1$$ would be a term.
Then we must define atomic formulas which are terms or "valid" combinations of those with relation symbols. Again with $L_G$, $$v_0*v_1\simeq e$$ would be an atomic formula (when not stated otherwise, all languages have the equality sign).
And from the atomic formulas we can define the formulas. For example $$\forall v_0(v_0*v_1\simeq e),\quad v_1\simeq e\vee \exists v_0(v_0\simeq v_1).$$ This formulas are called predicate formulas.
We say that a variable occur in a formula if it appear in the formula. Intuitively occurrence of a variable is bounded if "it is in the scope of some quantifier" and it is free otherwise. You can see examples in the above formulas. A formula is closed if it have no free occurrences of variables.
A theory $T$ of a first order language $L$ is a set of closed formulas of $L$.
Semantics
Okay, but this time how do you say which formulas are true or false? How do you give meaning to the formulas?
This is done with the structures. Given a first order language an $L$-structure is a nonempty set plus some functions and relations defined on it to give interpretations to functions, relations and constants symbols.
For example consider the language: $$L=\{R,s\}$$ where $R$ is a binary relation and $s$ is a binary function. Then $${\cal M}=\langle\Bbb R,\leq,+\rangle$$ is an $L$-structure.
In the structures you can interpret the atomic formulas, but this interpretation depends of the interpretation of the variables (if present) that you give. For example with the above language and $L$-structure the atomic formula $s(v_0,v_0)Rv_1$ is $$1+1\leq 1$$ when $v_0$ and $v_1$ are interpreted as $1$ and is $$0+0\leq 1$$ when $v_0$ is interpreted as $0$ and $v_1$ as 1.
Let's concentrate in closed formulas now. Given a first order language the structures decide whether or not a closed formula is true or false. Intuitively an $L$-structure $\cal M$ satisfies a closed formula $F$ if what is stated by the formula is indeed true in the structure. For example consider the language $$L=\{R,c\}$$ where $R$ is a binary relation and $c$ is a constant symbol, and the closed formula $$F=\forall v(vRc).$$ Consider the $L$-structures $${\cal M}=\langle \Bbb R,\geq,0\rangle,\qquad {\cal N}=\langle \Bbb N, \geq, 1\rangle.$$ Then notice that $F$ is not satisfied in $\cal{M}$ since for example $-1\not\geq 0$, but $\cal{N}$ does satisfies $F$ as you can see. In this case we write $${\cal N}\models F$$ and we say that $\cal{N}$ is a model for $F$.
Now, fix a first order language $L$.
- Given a theory $T$ of a language $L$ we say that an $L$-structure $\cal{M}$ is a model for $T$ if for each $F\in T$, ${\cal M}\models F$.
- We say that a formula $F$ is semantic consequence of a theory $T$, and write $T\vdash^\ast F$ if for each $L$-structure $\cal{M}$ $${\cal M}\models T\quad\text{implies}\quad {\cal M}\models F.$$
- A theory $T$ is universally valid if any $L$-structure is a model for $T$.
In the other hand the concept of proof can be formalized as well. Given a theory $T$ of $L$ a derivation of a formula $F$ is a finite sequence of formulas $(F_0,\ldots,F_n)$ with $F_n=F$ and where each formula $F_i$ satisfies:
- $F_i\in T$ or
- $F_i$ is a tautology (obtained by substituting the variables in the tautologies of propositional calculus by predicate formulas) or
- $F_i$ is in one of the axiom schemas (which are some special sets of universally valid formulas) or
- $F_i$ is deduced from previous formulas in the sequence by some of the rules of inference (for example a rule of inference is modus ponens: from $A$ and $A\implies B$ you can deduce $B$).
We say that a closed formula $F$ is syntactic consequence of a theory $T$ if $F$ can be derived from $T$. In that case we write $T\vdash F$.
One way to state the completeness theorem of first order logic is to say that being syntactic or being semantic consequence is the same thing. That is:
Given a theory $T$ and a formula $F$ of $L$, $$T\vdash^\ast F\quad\text{if and only if}\quad T\vdash F.$$
That is, if you want to proof that a formula $F$ can not be derived from a theory $T$ it is enough to exhibit a model of $T$ which is not a model of $F$.
The language of groups and the theory of groups.
Let $$L_G'=\{\ast\}\quad\text{and}\quad L_G=\{e,\ast\}$$ where $*$ is a binary function and $e$ is a constant symbol.
Notice that $L_G'\subseteq L_G$ and that the $L_G'$-structures are of the form $${\cal M'}=\langle M,+\rangle$$ where $+$ is a binary function defined on $M$ and is of course the interpretation of $\ast$ in $\cal M'$. But since $M$ must be nonempty there is a element $m$ that could be used as the interpretation of $c$. That is $${\cal M}=\langle M,m,+\rangle$$ is an $L_G$-structure.
When you have two languages $L'\subseteq L$ and an $L'$-structure $\cal M'$ and you keep the same underlying set, the functions, relations and constants that you already have, and add some new constants, functions and relations in order to obtain an $L$-structure $\cal M$, $\cal M$ is called an enrichment of $\cal M'$.
It must be intuitively clear, that if $F$ is a closed formula of $L'$ then $${\cal M'}\models F\qquad\text{iff}\qquad {\cal M}\models F.$$
Now, let $A$ be the closed formula of $L_G$ and $L_G'$ given by $$A=\forall v\forall w\forall x(v\ast(w\ast x)\simeq (v\ast w)\ast x).$$ Let $$T_G=\{A,\forall x(x\ast e\simeq e\ast x\simeq x),\forall x\exists y(x\ast y\simeq y\ast x\simeq e) \}.$$ You immediately recognize this as the axioms for of groups (notice the abuse of the language with $\simeq$, there must be some $\wedge$s).
But what if you try to write some reasonable axioms for groups with the language $L_G'$? Here you do not have the constant symbol $e$, so you must add something like: $$\begin{gather*} Id=\exists u \forall x(x\ast u\simeq u\ast x\simeq x)\\ In=\forall x \exists y\forall w(w\ast (x\ast y)\simeq w\ast (y\ast x)\simeq w) \end{gather*}$$ Let $$T_G'=\{A,Id,In\}.$$ If you start with $L_G'$ and $T_G'$, it turns out that the formula that says that the identity element is unique can be deduced from $T_G'$. So you can enrich the language to $L_G$ and then the models of $T_G'$ will be (with the right interpretation of $e$) exactly the models of $T_G$.
And, as you can see the formulas of $T_G$ are simpler. In fact with $L_G$ it is possible to have a theory of groups with a single elegant axiom (This is always possible, since the theory is finite and you can take the conjunction of the axioms, but that's not the axiom I'm talking about: look).
So it is easier to say things if your language is richer.
For your exercise, for sure it's supposed you must use $L_G$ and $T_G$. So you must follow what is given in the other answers.
Hope this helps.
To say that a set of axioms $T$ is independent is to say that for every $\varphi\in T$, there is a model of $T\setminus\{\varphi\}$ in which $\varphi$ is false, and another in which it is true. This is, of course, a consequence of the completeness theorem of first-order logic.
For example, in the theory of abelian groups the commutative axiom is independent of the others. $S_6$ is a non-abelian group, and the trivial group is an abelian group.