[proofplan]
Fix arbitrary variables $x$ and $y$ and prove the formula $(x+y)+z = x+(y+z)$ by the induction axiom of PA applied to the variable $z$. The base case is exactly the recursive equation $a+0=a$, used first with $a=x+y$ and then with $a=y$. The induction step uses the recursive equation $a+Sb=S(a+b)$ on both sides, then applies equality substitution through the successor symbol. Since $x$ and $y$ were arbitrary, universal generalization gives the desired closed theorem of PA.
[/proofplan]
[step:Fix the parameters and define the induction formula]
Let $x$ and $y$ be arbitrary variables of the language of PA. Define the one-variable formula $\varphi(z)$ by
\begin{align*}
\varphi(z) \;:\!\iff\; (x+y)+z = x+(y+z).
\end{align*}
We will prove $\varphi(z)$ for all $z$ by applying the induction axiom schema of PA to this formula.
[guided]
We want to prove a universally quantified statement about three variables. The addition recursion in PA is recursive in the second argument, so the natural variable for induction is $z$, the final addend. Thus we temporarily regard $x$ and $y$ as fixed parameters and define the formula
\begin{align*}
\varphi(z) \;:\!\iff\; (x+y)+z = x+(y+z).
\end{align*}
This is a legitimate formula of the language of PA with free variables among $x,y,z$. The induction axiom schema may be applied to any formula of the language, including formulas with parameters, so it is enough to prove the base instance $\varphi(0)$ and the induction implication $\varphi(z)\to \varphi(Sz)$.
[/guided]
[/step]
[step:Prove the base case using the right-zero equation for addition]
We prove $\varphi(0)$, namely
\begin{align*}
(x+y)+0 = x+(y+0).
\end{align*}
By the addition axiom $a+0=a$ with $a=x+y$,
\begin{align*}
(x+y)+0 = x+y.
\end{align*}
By the same axiom with $a=y$,
\begin{align*}
y+0 = y.
\end{align*}
Substituting this equality into the term $x+(y+0)$ gives
\begin{align*}
x+(y+0)=x+y.
\end{align*}
By transitivity and symmetry of equality,
\begin{align*}
(x+y)+0 = x+(y+0).
\end{align*}
Thus PA proves $\varphi(0)$.
[guided]
The base case asks for associativity when the third argument is $0$:
\begin{align*}
(x+y)+0 = x+(y+0).
\end{align*}
The recursive definition of addition in PA includes the axiom $a+0=a$ for every term $a$. Applying it to the term $x+y$ gives
\begin{align*}
(x+y)+0 = x+y.
\end{align*}
Applying the same axiom to the term $y$ gives
\begin{align*}
y+0 = y.
\end{align*}
Equality in PA is substitutive for function symbols, so from $y+0=y$ we may substitute equals into the context $x+(\,\cdot\,)$ and obtain
\begin{align*}
x+(y+0)=x+y.
\end{align*}
Both sides of the desired equality are therefore equal to $x+y$. Using symmetry and transitivity of equality, PA derives
\begin{align*}
(x+y)+0 = x+(y+0).
\end{align*}
This is exactly $\varphi(0)$.
[/guided]
[/step]
[step:Derive the successor case from the induction hypothesis]
Assume the induction hypothesis
\begin{align*}
(x+y)+z = x+(y+z).
\end{align*}
We prove
\begin{align*}
(x+y)+Sz = x+(y+Sz).
\end{align*}
By the recursive addition axiom $a+Sb=S(a+b)$ with $a=x+y$ and $b=z$,
\begin{align*}
(x+y)+Sz = S((x+y)+z).
\end{align*}
By equality substitution through the successor symbol applied to the induction hypothesis,
\begin{align*}
S((x+y)+z)=S(x+(y+z)).
\end{align*}
By the recursive addition axiom with $a=y$ and $b=z$,
\begin{align*}
y+Sz = S(y+z).
\end{align*}
Substituting this equality into the context $x+(\,\cdot\,)$ gives
\begin{align*}
x+(y+Sz)=x+S(y+z).
\end{align*}
By the recursive addition axiom with $a=x$ and $b=y+z$,
\begin{align*}
x+S(y+z)=S(x+(y+z)).
\end{align*}
Combining these equalities by transitivity and symmetry yields
\begin{align*}
(x+y)+Sz = x+(y+Sz).
\end{align*}
Hence PA proves $\varphi(z)\to \varphi(Sz)$.
[guided]
Assume the induction hypothesis
\begin{align*}
(x+y)+z = x+(y+z).
\end{align*}
The goal is the same associativity formula with $Sz$ in place of $z$:
\begin{align*}
(x+y)+Sz = x+(y+Sz).
\end{align*}
We first rewrite the left-hand side using the recursive addition axiom $a+Sb=S(a+b)$. With $a=x+y$ and $b=z$, PA proves
\begin{align*}
(x+y)+Sz = S((x+y)+z).
\end{align*}
Now the induction hypothesis says that the term inside this successor is equal to $x+(y+z)$. Equality is substitutive for the function symbol $S$, so PA derives
\begin{align*}
S((x+y)+z)=S(x+(y+z)).
\end{align*}
Next we rewrite the right-hand side. Applying the recursive addition axiom with $a=y$ and $b=z$ gives
\begin{align*}
y+Sz = S(y+z).
\end{align*}
Substitution into the context $x+(\,\cdot\,)$ gives
\begin{align*}
x+(y+Sz)=x+S(y+z).
\end{align*}
Applying the recursive addition axiom once more, now with $a=x$ and $b=y+z$, gives
\begin{align*}
x+S(y+z)=S(x+(y+z)).
\end{align*}
Thus the left-hand side $(x+y)+Sz$ is equal to $S(x+(y+z))$, and the right-hand side $x+(y+Sz)$ is also equal to $S(x+(y+z))$. By symmetry and transitivity of equality, PA proves
\begin{align*}
(x+y)+Sz = x+(y+Sz).
\end{align*}
This is precisely $\varphi(Sz)$, so PA proves the implication $\varphi(z)\to\varphi(Sz)$.
[/guided]
[/step]
[step:Apply induction and universally generalize the parameters]
From the previous steps, PA proves
\begin{align*}
\varphi(0)
\end{align*}
and
\begin{align*}
\forall z\,(\varphi(z)\to \varphi(Sz)).
\end{align*}
By the induction axiom schema applied to $\varphi$, PA proves
\begin{align*}
\forall z\,\varphi(z),
\end{align*}
that is,
\begin{align*}
\forall z\,\bigl((x+y)+z=x+(y+z)\bigr).
\end{align*}
Since $x$ and $y$ were arbitrary parameters and no undischarged assumptions about them remain, universal generalization gives
\begin{align*}
\forall x\,\forall y\,\forall z\,\bigl((x+y)+z=x+(y+z)\bigr).
\end{align*}
Therefore PA proves associativity of addition.
[/step]
