Solution (source code)

= Solution

The <axiom of infinity> asserts that an <inductive set> exists: some <set> $I$ contains $0=\varnothing$ and contains $x^+=x\cup\{x\}$ whenever it contains $x$. Inside one such $I$, <axiom of separation> defines
$$
\omega=\{x\in I:x\text{ belongs to every inductive subset of }I\}.
$$
This <intersection> is itself inductive and is contained in every <inductive set>, by intersecting that <set> with $I$. It is therefore the <set> of <natural numbers>. If a property holds at $0$ and passes from $n$ to $n^+$, <axiom of separation> forms the <subset> of $\omega$ on which it holds. That <subset> is inductive, so must equal $\omega$. This proves <mathematical induction>, including properties with <set> parameters.

<Recursion> on $\omega$ defines the arithmetic operations by
$$
m+0=m,\qquad m+n^+=(m+n)^+,\qquad
m\cdot0=0,\qquad m\cdot n^+=m\cdot n+m.
$$
Existence and uniqueness follow from the <recursion theorem on the natural numbers>.

For <associativity> of <addition> fix $m,n$ and induct on $k$. At $k=0$ both sides equal $m+n$. If the equality holds at $k$, then
$$
m+(n+k^+)=m+(n+k)^+=(m+(n+k))^+
=((m+n)+k)^+=(m+n)+k^+.
$$
Thus
$$
\boxed{m+(n+k)=(m+n)+k.}
$$
Every step after the <induction hypothesis> is a defining successor equation, so <commutativity> has not been used prematurely.