Let $P(k)$ be a well formulated mathematical statement (in the FOL language of ZFC) involving $k\in \mathbb{N}$. Suppose I want to show that $P(k)$ holds for all $1\leq k \leq m$ for some fixed $m\in \mathbb{N}$.
One approach is to use induction. To do this I can define $A=\{ k \in \mathbb{N} :1\leq k \leq m \wedge P(k) \}$ and $B=\{ k \in \mathbb{N}: n> m \}$. I can then show that $A\cup B = \mathbb{N}$ by mathematical induction and obtain the result.
But another approach (e.g. Induction on finite subset of natural numbers) says that we don't need induction in this case. The idea being that if you can show that $P(1)$ holds and that $P(k)\implies P(k+1)$ holds for all $1\leq k <m$ then you can apply modus ponens a finite number of times to obtain the result.
I know that the first proof can be written in formal language but am not sure about the second approach. The problem seems to be the sentence "apply modus ponens a finite number of times to obtain the result" because it is not clear to me how this can be formalized in FOL.
Is the second approach really valid?
EDIT. In fact using the second approach I can prove the PMI itself:
Suppose $P(1)$ holds and that $P(k)\implies P(k+1)$ for all $k \in \mathbb{N}$. Assume there exist $m \in \mathbb{N}$ such that $P(m)$ does not hold. Applying modus ponens $m$ times I deduce that $P(m)$ holds, a contradiction. Hence $P(k)$ holds for all $k \in \mathbb{N}$.
In a finite domain of discourse (with say, $k$ objects), the notion of induction $(1)$, can be captured in the form of $(2)$, which is a lists finite set of implications, and a single base case, as premises.
$$p(1),\forall n.\big(p(n)\implies p(n+1)\big)\vdash \forall n. p(n)\tag{1}$$
$$p(x_1),\big(p(x_1)\implies p(x_2)\big),\dots,\big(p(x_{k-1})\implies p(x_k)\big)\vdash \forall x. p(x)\tag{2}$$
To show that $(2)$ is a valid rule of inference (in a finite language*), it is sufficient to construct a formal proof from its premises to its conclusion. This is done by applying modus ponens to each of the implications, then applying domain closure to get the desired result.
\begin{align} &1.&p(x_1)&~~~~\text{P}\\ &2.&p(x_1)\implies p(x_2)&~~~~\text{P}\\ &&\dots\\ &k.&p(x_{k-1})\implies p(x_{k})&~~~~\text{P}\\ &k+1.&p(x_2)&~~~~\text{Modus ponens } 1,k-1\\ &&\dots\\ &2k-1.&p(x_k)&~~~~\text{Modus ponens } 2k-3,2k-2\\ &2k.&\forall x.\big(p(x)\big)&~~~~\text{Domain closure } 1,k+1,\dots,2k-1 \end{align}
For instance, in a language with just $3$ objects, abby, bess, cody, we can write:
\begin{align} &1.&p(abby)&~~~~\text{P}\\ &2.&p(abby)\implies p(bess)&~~~~\text{P}\\ &3.&p(bess)\implies p(cody)&~~~~\text{P}\\ &4.&p(bess)&~~~~\text{Modus ponens } 1,2\\ &5.&p(cody)&~~~~\text{Modus ponens } 3,4\\ &6.&\forall x.\big(p(x)\big)&~~~~\text{Domain closure } 1,4,5 \end{align}
Edit: You can apply this same technique to a finite set, but you need to specify the set in question.
\begin{align} &0.&X=\{abby,bess,cody\}&~~~~\text{P}\\ &1.&p(abby)&~~~~\text{P}\\ &2.&p(abby)\implies p(bess)&~~~~\text{P}\\ &3.&p(bess)\implies p(cody)&~~~~\text{P}\\ &4.&p(bess)&~~~~\text{Modus ponens } 1,2\\ &5.&p(cody)&~~~~\text{Modus ponens } 3,4\\ &6.&\forall x\in X.\big(p(x)\big)&~~~~1,4,5 \end{align}