Consider the two following formulations of the principle of mathematical induction.
First formulation Let there be given a set $S$ with the following properties :
(i) 1 $\in S$,
(ii) $n \in S \implies n+1 \in S$.
Then $\mathbb{N} \subseteq S$.
Second formulation If
(i) $\phi(0)$,
(ii) $\phi(n) \implies \phi(n+1)$,
then $\phi(n) \space \forall n$.
That only one of these two formulations assumes that $0 \in \mathbb{N}$ is irrelevant.
The first formulation is taken from Landau's Foundations of Analysis and is a second-order formulation since, in particular, we quantify over all subsets of $\mathbb{N}$.
The second formulation is taken from Suppes' Axiomatic Set Theory, in which he constructs the set of natural numbers from the axioms of ZF. This formulation of the mathematical induction principle is then a theorem schema. As I understand it, $\phi(n)$ is a predicate (or a property), so it is a well-formed formula of the first-order system of set theory developed in the book.
Are these two formulations equivalent ? After proving the second formulation, Suppes gives as a theorem the "set formulation of the principle of induction", that is, the first formulation given here with $0 \in S$ as (i) instead of $1 \in S$ (hence ZF, because it's variables range over the class of all sets, is strong enough to include the second-order Peano's induction axiom ?). It seems to me that since the set of well-formed formulas of a given first-order language is countable, but $\mathcal P \left({\mathbb{N}}\right)$ isn't, the first formulation should be stronger than the second one. In fact, it seems to me like the second formulation is one of the axioms of first-order arithmetic. Where am I wrong ?
The usual version of the second formulation of induction, which one deduces from ZF, allows the formula $\phi(n)$ to have other free variables, in addition to $n$. So the schema that is provable in ZF is, when written in more detail, $$ \forall\vec x[(\phi(0,\vec x)\land\forall n\in\mathbb N(\phi(n,\vec x)\to\phi(n+1,\vec x)))\to \forall n\in\mathbb N\,\phi(n,\vec x)], $$ where $\vec x$ represents whatever variables other than $n$ are free in $\phi$. Thus, although there are only countably many formulas $\phi$ and therefore only countably many statements in this schema, each of these statements can have uncountably many (in fact, a proper class of) instances corresponding to different values for $\vec x$. In particular, by taking $\phi$ to be the formula $n\in x$ (with just one additional variable $x$), we get your first formulation of induction.