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?
Yes, commutativity of addition is a logical consequence of the other field axioms. Nothing wrong with being a little bit redundant.
The missing lemma for the proof:
Let $x \in k$. Then
$$0 = 0 \cdot x = (1 + (-1))\cdot x = 1 \cdot x + (-1) \cdot x = x + (-1)\cdot x$$
Similarly,
$$0 = 0 \cdot x = (-1 + 1)\cdot x = (-1) \cdot x + 1 \cdot x = (-1)\cdot x + x$$
So $(-1)\cdot x$ is the additive inverse of $x$,
$$-x = (-1) \cdot x$$