[proofplan] The proof is a formal derivation inside the proof system for first-order Peano Arithmetic. We take the induction axiom instance associated to the formula $\varphi(x,y_1,\dots,y_k)$, combine the two assumed PA-derivations by conjunction introduction, and then use modus ponens to obtain the universal conclusion. Since the parameter variables $y_1,\dots,y_k$ occur in no undischarged assumptions, universal generalization may be applied to them afterward. [/proofplan]

[step:Instantiate the induction axiom schema with the formula $\varphi$]Let $y$ abbreviate the finite tuple $(y_1,\dots,y_k)$. The induction axiom schema of $\mathrm{PA}$ has, for the formula $\varphi(x,y)$, the following instance: \begin{align*} \bigl(\varphi(0,y)\wedge \forall x(\varphi(x,y)\to \varphi(Sx,y))\bigr)\to \forall x\,\varphi(x,y). \end{align*} Because this is an axiom instance of $\mathrm{PA}$, it is derivable in $\mathrm{PA}$: \begin{align*} \mathrm{PA}\vdash \bigl(\varphi(0,y)\wedge \forall x(\varphi(x,y)\to \varphi(Sx,y))\bigr)\to \forall x\,\varphi(x,y). \end{align*}[/step]

[guided]Let $y$ denote the tuple of all parameter variables $(y_1,\dots,y_k)$. The point of allowing parameters is that the induction schema is not restricted to formulas with only one free variable. It applies to every $\mathcal L_{\mathrm{PA}}$-formula $\varphi(x,y)$, where $x$ is the variable over which induction is performed and $y$ is carried along as a tuple of parameters. For this specific formula, the induction axiom instance is \begin{align*} \bigl(\varphi(0,y)\wedge \forall x(\varphi(x,y)\to \varphi(Sx,y))\bigr)\to \forall x\,\varphi(x,y). \end{align*} This formula is an axiom of $\mathrm{PA}$ by the induction axiom schema itself. Therefore it has a PA-proof: \begin{align*} \mathrm{PA}\vdash \bigl(\varphi(0,y)\wedge \forall x(\varphi(x,y)\to \varphi(Sx,y))\bigr)\to \forall x\,\varphi(x,y). \end{align*} The role of this step is to expose exactly where induction enters: not as a separate rule of inference, but as a particular axiom instance already available inside $\mathrm{PA}$.[/guided]

[step:Derive the antecedent of the induction instance]By hypothesis, \begin{align*} \mathrm{PA}\vdash \varphi(0,y) \end{align*} and \begin{align*} \mathrm{PA}\vdash \forall x(\varphi(x,y)\to \varphi(Sx,y)). \end{align*} Applying conjunction introduction to these two PA-derivations gives \begin{align*} \mathrm{PA}\vdash \varphi(0,y)\wedge \forall x(\varphi(x,y)\to \varphi(Sx,y)). \end{align*}[/step]

[guided]The antecedent of the induction axiom instance has two conjuncts. The first conjunct is the base case: \begin{align*} \varphi(0,y). \end{align*} The second conjunct is the induction step: \begin{align*} \forall x(\varphi(x,y)\to \varphi(Sx,y)). \end{align*} Both are PA-theorems by the hypotheses of the theorem: \begin{align*} \mathrm{PA}\vdash \varphi(0,y) \end{align*} and \begin{align*} \mathrm{PA}\vdash \forall x(\varphi(x,y)\to \varphi(Sx,y)). \end{align*} The logical rule of conjunction introduction says that from derivations of $A$ and $B$ with no additional undischarged assumptions, one may form a derivation of $A\wedge B$. Applying that rule with \begin{align*} A := \varphi(0,y) \end{align*} and \begin{align*} B := \forall x(\varphi(x,y)\to \varphi(Sx,y)) \end{align*} yields \begin{align*} \mathrm{PA}\vdash \varphi(0,y)\wedge \forall x(\varphi(x,y)\to \varphi(Sx,y)). \end{align*} This is exactly the antecedent needed to use the induction axiom instance from the previous step.[/guided]

[step:Apply modus ponens to obtain the universal conclusion]From the previous two steps, $\mathrm{PA}$ proves both \begin{align*} \bigl(\varphi(0,y)\wedge \forall x(\varphi(x,y)\to \varphi(Sx,y))\bigr)\to \forall x\,\varphi(x,y) \end{align*} and \begin{align*} \varphi(0,y)\wedge \forall x(\varphi(x,y)\to \varphi(Sx,y)). \end{align*} Applying modus ponens gives \begin{align*} \mathrm{PA}\vdash \forall x\,\varphi(x,y). \end{align*} Substituting back $y=(y_1,\dots,y_k)$, this is \begin{align*} \mathrm{PA}\vdash \forall x\,\varphi(x,y_1,\dots,y_k). \end{align*} Thus the induction rule is admissible in $\mathrm{PA}$.[/step]

[guided]We now have the two pieces required for modus ponens. First, $\mathrm{PA}$ proves the conditional supplied by the induction axiom instance: \begin{align*} \mathrm{PA}\vdash \bigl(\varphi(0,y)\wedge \forall x(\varphi(x,y)\to \varphi(Sx,y))\bigr)\to \forall x\,\varphi(x,y). \end{align*} Second, $\mathrm{PA}$ proves the antecedent of that conditional: \begin{align*} \mathrm{PA}\vdash \varphi(0,y)\wedge \forall x(\varphi(x,y)\to \varphi(Sx,y)). \end{align*} The rule of modus ponens says that from derivations of $A\to B$ and $A$, one may infer a derivation of $B$. Here \begin{align*} A := \varphi(0,y)\wedge \forall x(\varphi(x,y)\to \varphi(Sx,y)) \end{align*} and \begin{align*} B := \forall x\,\varphi(x,y). \end{align*} Therefore \begin{align*} \mathrm{PA}\vdash \forall x\,\varphi(x,y). \end{align*} Replacing the abbreviation $y$ by the tuple $(y_1,\dots,y_k)$ gives \begin{align*} \mathrm{PA}\vdash \forall x\,\varphi(x,y_1,\dots,y_k). \end{align*} This proves that whenever the base case and induction step are already derivable in $\mathrm{PA}$, the universally quantified conclusion is also derivable in $\mathrm{PA}$. Hence induction may be used as an admissible derived rule, even though the official axiomatization presents induction as an axiom schema.[/guided]

[step:Universally generalize over the parameter variables when a closed theorem is desired] If one wants the fully closed form, the variables $y_1,\dots,y_k$ occur in no undischarged assumptions, because the derivation just constructed is a PA-proof from axioms alone. Therefore repeated universal generalization gives \begin{align*} \mathrm{PA}\vdash \forall y_1\cdots\forall y_k\forall x\,\varphi(x,y_1,\dots,y_k). \end{align*} For $k=0$, this final generalization step is vacuous. [/step]