$a+b=a$, if $b=0$
$a+b=S(a)+S^{-1}(b)$, if $b\not=0$
Here a and b are natural numbers defined according to the Peano axioms, while S represents the successor function.
Basically, I am trying to prove that $\forall a\in N_0\forall b\in N_0(a+b=b+a)$
I am assuming this is supposed to be proved by induction, but I am struggling to come up with a proof.
I am not 100% clear on how the $S^{-1}$ is to be dealt with formally, but let's assume that your axioms can be rephrased as:
$\forall x \ x + 0 = x \tag{1}$
$\forall x \forall y \ x + S(y) = S(x) + y \tag{2}\label{2}$
or that you can get to these through a fairly easy derivation.
With that, one idea now is to derive the traditional Peano axioms for addition:
$$\forall x \ x + 0 = x \tag{PA1}$$
$$\forall x \forall y \ x + S(y) = S(x + y) \tag{PA2}\label{PA2}$$
In other words, we just need to derive what is traditionally the second axiom for addition.
To do that, they key is to show that:
$$\forall y \forall x \ S(x) + y = S(x + y) \tag{*}\label{*}$$
We can do this by induction over the outside $y$, i.e. show that:
$\forall x \ S(x) + 0 = S(x + 0) \tag{Base}$
$$\text{For any } b: \forall x \ S(x) + b = S(x + b) \to \forall x \ S(x) + S(b) = S(x + S(b)) \tag{Step}$$
For the Base, a simple universal proof will suffice.
For the inductive step, consider some arbitrary $b$, and assume tyhe inductive hypothesis:
$$\forall x \ S(x) + b = S(x + b) \tag{I.H.}\label{I.H.}$$
OK, so now need to show:
$$\forall x \ S(x) + S(b) = S(x + S(b))$$
Again, a good old universal proof will suffice. Consider any arbitrary $a$.
First note that since:
$$a + S(b) \overset{\eqref{2}}{=} S(a) + b$$
we have:
$$S(a) + b = a + S(b) \tag{3}\label{3}$$
So that means:
$$S(a) + S(b) \overset{\eqref{2}}{=} S(S(a)) + b \overset{\eqref{I.H.}}{=} S(S(a) + b) \overset{\eqref{3}}{=} S(a + S(b))$$
which is what we were looking for, thus completing the inductive step.
Once you have $\eqref{*}$, it's now trivial to show $\eqref{PA2}$.
And now you can do all the usual proofs involving the traditional Peano axioms, including commutativity of addition.