I seem to have found a proof that the commutativity of $+$ follows from the other field axioms. It is as follows:
Let $(k,+,\cdot)$ be a structure satisfying all field axioms except commutativity of addition, with $a,b\in k$. Then
1) $(a + b)\in k$ and $(b+a)\in k$ (closure of addition)
2) $-(a+b)\in k$ and $-(b+a)\in k$ (invertible addition)
3) $(a+b) + [-(b+a)] =(a+b) + (-b) + (-a)$ (distributivity of $\cdot$ over $+$)
4) $(a+b) + (-b) + (-a) = a + (b + (-b)) + (-a)$ (associativity of $+$)
5) $a + (b + (-b)) + (-a) = a + 0 + (-a) = a + (-a)$ (invertibility and identity of $+$)
6) $(a + b) + [-(b+a)] = 0$ (identity of $+$)
7) $(a+b) = (b+a)$ (invertibility of $+$) $\,\square$
But commutativity is a field axiom, so it must be necessary. Given that, what is wrong with this proof? Can the final conclusion (7) not be drawn without commutativity?
Best Answer
Since we are talking about Fields here and the field axioms are an extension of the ring axioms (a field can be defined as a commutative ring with $1$), you are correct to see redundancy.
However, since the field axioms are constructed from ring axioms and in rings the property is not redundant, it's justified to keep this redundancy. The essential part of the field axioms that generates the redundancy is that $1\in F$ (the field has a multiplicative identity) and it is a ring.
Without this property $-(b+a)$ (the additive inverse of $b+a$) is not guaranteed to be $-1 \cdot (b+a)$ since $-1$ may not even exist. Instead, $-(b+a) = (-a)+(-b)$ because $b+a+(-a)+(-b)=0$.
We can prove that for a Ring to have commutative addition it suffices that it has a $1$:
$$\begin{align*} a+a+b+b & = (1+1)\cdot a+(1+1)\cdot b & \text{left-distributivity}; 1\cdot a = a \\ & = (1+1)\cdot(a+b) & \text{right-distributivity}\\ &= 1\cdot(a+b) + 1\cdot(a+b) & \text{left-distributivity}\\ & = a+b+a+b &\text{right-distributivity} \\ \Rightarrow a+b&=b+a & \text{cancellation} \end{align*}$$ Proof taken from here.
Now although the property is redundant for fields, it isn't in the context of a commutative ring so it's a good idea to still keep all the (non-redundant) ring axioms for consistency since every field is a ring.