Formulation of the (axiom of) mathematical induction 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 ?
 A: This is only a partial answer; I can't quite tell you where your problem is, but I can provide some useful information.
It's probably a good idea to be pedantic about what $S$ in the first formulation and $\phi$ in the second formulation are. I suppose what is intended is that the first formulation is higher-order, so implicitly prefixed with a quantifier $\forall S$, whereas the second formulation is first-order and actually an axiom schema rather than a single axiom – that is to say, for any choice of $\phi$, the second formulation is an axiom, and we take all of these axioms as part of our theory.
As you've correctly observed, $\forall S$ quantifies over more than the axiom schema can cover, because not every subset of $\mathbb N$ can be specified as a formula.
This difference matters. The second order formulation, I'm told, has a unique model (up to isomorphism), but the Löwenheim–Skolem theorem says that the first-order formulation (and indeed, a far more general class of first-order theories) must have non-isomorphic models. Even without considering different cardinalities, the Compactness Theorem will give countable models of this theory that nevertheless contain "exotic" natural numbers. These are called non-standard models.
Non-standard models are weird. Tennenbaum's theorem says that they cannot have computable operations.
I suspect that what is going on here is that if your natural numbers are non-standard, your set theory looks very weird, and in particular will believe its own formulation of second-order arithmetic despite the fact that to an external observer it's obviously false. 
A: 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.
