[proofplan] We prove the formula $0+x=x$ by induction on $x$ inside $\mathrm{PA}$. The base case is the defining axiom $y+0=y$ applied to $y=0$. For the successor step, the recursive axiom for addition rewrites $0+S(x)$ as $S(0+x)$, and equality congruence for the successor function transports the induction hypothesis $0+x=x$ to $S(0+x)=S(x)$. The induction schema then yields the universal statement. [/proofplan] [step:Choose the induction formula] Let $\varphi(x)$ denote the first-order formula \begin{align*} 0 + x = x. \end{align*} We will prove the two premises required by the induction schema for this formula: \begin{align*} \varphi(0) \qquad\text{and}\qquad \forall x\,(\varphi(x) \to \varphi(S(x))). \end{align*} [/step] [step:Prove the base case from the defining axiom for addition] The defining axiom for addition with right argument $0$ is \begin{align*} \forall y\, (y + 0 = y). \end{align*} Instantiating this axiom with $y := 0$ gives \begin{align*} 0 + 0 = 0. \end{align*} This is precisely $\varphi(0)$. [/step] [step:Derive the successor case from the recursive axiom for addition] Fix an arbitrary variable $x$ and assume the induction hypothesis \begin{align*} 0 + x = x. \end{align*} The recursive defining axiom for addition is \begin{align*} \forall y\,\forall z\,\bigl(y + S(z) = S(y + z)\bigr). \end{align*} Instantiating this axiom with $y := 0$ and $z := x$ gives \begin{align*} 0 + S(x) = S(0 + x). \end{align*} By equality congruence for the unary function symbol $S$, the induction hypothesis $0+x=x$ implies \begin{align*} S(0+x) = S(x). \end{align*} Using transitivity of equality on the two displayed equalities yields \begin{align*} 0 + S(x) = S(x). \end{align*} This is exactly $\varphi(S(x))$. Since $x$ was arbitrary, we have proved \begin{align*} \forall x\,(\varphi(x) \to \varphi(S(x))). \end{align*} [/step] [step:Apply the induction schema to conclude the universal identity] The induction schema of $\mathrm{PA}$ applied to the formula $\varphi(x)$ gives \begin{align*} \bigl(\varphi(0) \land \forall x\,(\varphi(x) \to \varphi(S(x)))\bigr) \to \forall x\,\varphi(x). \end{align*} The previous two steps established the antecedent, so modus ponens gives \begin{align*} \forall x\,\varphi(x). \end{align*} Substituting the definition of $\varphi(x)$, this is \begin{align*} \forall x\, (0 + x = x). \end{align*} Thus $\mathrm{PA} \vdash \forall x\, (0+x=x)$. [/step]