The usual induction used in the "traditional mathematics" (that does not care about logic and foundations as, for example, basic real analysis), reads as follows.
Principle of mathematical induction (PI): If $X$ is a subset of $\mathbb N$ such that
- $0\in X$
- $n\in X\Rightarrow n+1\in X$
then $X=\mathbb N$.
I'd like to understand how this "set-theoretic formulation" relates to the formal first and second order formulations.
Using this post and Wikipedia as reference, we have (correct me if I'm wrong):
First order induction schema: it includes the axiom $$(\phi(0) \land\forall n(\phi(n)\to\phi(n+1)))\to \forall n\phi(n),\tag{1}$$ for every first-order formula $\phi$.
Second order induction axiom: $$\forall P((P(0)\land \forall n(P(n)\to P(n+1))\to \forall nP(n)).\tag{2}$$
Question 1: Take $X\subset \mathbb N$. Since $(2)$ is valid for all $P$, it is valid for the case where $P(x)$ is the sentence "$x\in X$". Thus, $(2)$ implies the PI. Is this reasoning correct?
Question 2: Take $X\subset \mathbb N$ that have the form $\{n\in \mathbb N\mid \psi(n) \}$, where $\psi$ is a first-order formula. Since $\psi$ is a first-order formula, $(1)$ is valid for $\phi=\psi$. Since "$\psi(x)$" is equivalent to "$x\in X$", $(1)$ implies the PI provided that $X$ can be defined by a first-order formula. Is this reasoning correct?
Question 3: Can the first order induction schema be used to obtain the PI without any restriction on $X$? If not, is the "traditional mathematics" always based on the second-order version?
Question 4: For the practical purposes of the "traditional mathematics", would the restriction of the PI to the cases where $X$ is definable by first order formulas be too severe? There are results that cannot be proved with this restriction?