Can finite induction be independent of mathematical induction? Suppose we have a property $P(n)$ pertaining to natural numbers and $P(n) \to P(n+1)$.
We know by mathematical induction that $P(N)$ implies $P$ being true for all natural numbers greater than or equal to $N$.
It is an obvious consequence of this that for a finite number of natural numbers greater than or equal to $N$, $P$ is also true. I am wondering, however, that whether this &quot;finite induction&quot; can be applied even if we didn't know mathematical induction principle. This might seem trivial, just like $P(1) \to P(2)$, $P(2) \to P(3)$ and so on, but I don't know any logical rules approving this...
We can prove the meta-theorem that in any logical system which lets you derive $Q$ from $P$ and $P \implies Q$, there is a proof of any given $P(n)$ from a base case less than $n$ and the induction step $P(n) \implies P(n+1)$. It is not necessary that the logical system have induction as an axiom.
In that logical system, such proofs will look like

Prove $P(1)$.
Prove $P(1) \implies P(2)$.
Prove $P(2) \implies P(3)$.
Prove $P(3) \implies P(4)$.
Prove $P(4) \implies P(5)$.
Conclude $P(2)$, then $P(3)$, then $P(4)$, then $P(5)$ by modus ponens.

It will be able to prove any given $P(n)$, and the meta-theorem tells us that it will be able to prove any given $P(n)$. Without the axiom of induction, it will not be able to prove $\forall n\ge 1\, P(n)$.
Induction will hold an any set $X$ (possibly finite) with $x_0\in X$ (the &quot;first&quot; element) and $f: X \to X$ (the &quot;successor&quot; function) such that:
$~~~~~~X=\{ x_0, f(x_0), f(f(x_0)), \cdots \} $
We have:
$~~~~~~\forall P\subset X: [x_0\in P \land \forall a\in P:[ f(a)\in P] \implies P=X]$