Formulation of axiom of induction? Tthe axiom of induction has the following second order formulation:
$$\forall \phi :\left(\phi(0)\wedge \forall n\in \mathbb{N} :\left( \phi(n)\Rightarrow \phi(n+1)\right)\right)\Rightarrow \forall n\in \mathbb{N}: \phi(n)$$
Here $\phi(n)$ is a formula which is a result of (properly) replacing one of the free variables in $\phi$ with $n$ , but obviously in the above axiom the same variable was replaced with $0,n$ and $n+1$.
The above could better be formulated as 
$$\forall \phi(x) :\left(\phi[x/0]\wedge \forall n\in \mathbb{N} :\left( \phi[x/n]\Rightarrow \phi[x/n+1]\right)\right)\Rightarrow \forall n\in \mathbb{N}: \phi[x/n]$$
where the implicit replace same variable condition was made explicit. But there is still a meta-theoretical $\phi(x)$ which means $x$ is a free variable in $\phi$ and $\phi[x/y]$ which is the formula that is a result of proper replacement of $x$ in $\phi$ with $y$. (So $x$ is not an object but a label.)
Question:
can this axiom be formulated without meta-logical side-notes? (because as far as I know x being a free variable in $\phi$ is not a valid sentence in any formal logic)?
Note: I know about the other formulation with sets but still not satisfactory as $x\in \{y:\phi\}$ is defined as $\phi[y/x]$.
 A: Language in Question
I think the question cannot be answered as stated since there is a crucial part of information missing: what is the object-language in question? Since you want to formalize the induction axiom in this object-language. 
Insofar, I assume the following (usual) object-language since the theory you're interested in is probably second-order arithmetic:
$$ \mathcal L = \{0, s, +, \cdot, <, \in\}$$
This means: all those symbols can be used to build up formulas within the object-language. 
Formulating Induction
Given $\mathcal L$ we can formulate:
$$\forall X. (0 \in X \wedge (\forall n . n \in X \to s(n) \in X)) \to \forall n . n \in X$$
This is a statement merely in the object-language. 
Its meaning is what defines natural induction if taken to account that using the usual comprehension principle we can capture every (almost; if not paradoxical) property as membership of a specific set. But this fact is nothing we have to make to write down the sentence above.
If the sentence captures what we understand under natural induction though is a philosophical question IMO. 
