[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*}
[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]
[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*}
[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]
[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}$.
[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]
[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]
