Parameters in arithmetic induction axiom schemas The induction schema of Peano Arithmetic is standardly given as the universal closure of $\phi(0)\land \forall x (\phi(x)\rightarrow \phi(x+1)) \rightarrow \forall x\phi(x)$.  However, since the language of arithmetic has a name for every standard number, it is not obvious (to a beginner like me) why parameters are necessary in the induction schema; why not restrict to the case where $x$ is the only free variable in $\phi$?  


*

*Does having parameters in the induction schema really make the system stronger, and, if so, how is that proven?  

*Are there natural theorems that can only or most easily be proven using the stronger system?  

*Is the weaker system of any interest?

 A: The two theories are equivalent. To see this, let's assume that we have the parameter-free induction, and suppose that $\phi(x,y)$ is a formula with two free variables. Suppose we have a model $M$, satisfying the parameter-free induction, and there is a $b\in M$ such that $\phi(x,b)$ obeys the hypothesis of the induction scheme with parameter $b$, but not the conclusion. I claim that there is a least such $b$ in $M$. The reason is that the collection of such $b$ violating the induction scheme for $\phi(x,b)$ with parameter $b$ is a parameter-free definable subset of $M$, since this property is expressible, but the parameter-free induction scheme proves that every nonempty definable set $B$ has a least member, because otherwise the assertion $\psi(x)$ expressing that $x$ is below all members of $B$ would be inductive and hence universal, contrary to $B$ being nonempty. So there is a least such $b$.
In particular, the least such $b$ is actually definable, and so we do not actually need it as a parameter after all, and so the induction scheme for $\phi(x,b)$ follows by the parameter-free induction scheme. So there can be no such $b$ for which the parameter-induction scheme fails.
Thus, the theory of parameter-free induction implies the full theory you mention. 
A: While parameter-free induction and parameterized induction are equivalent, there is an important subtlety which often justifies the addition of parameters.
Suppose that $\phi(x,p)$ is such that $$\exists p(\phi(0,p) \land \forall x(\phi(x,p) \to \phi(x+1,p)) \land \lnot \forall x \phi(x,p)).$$ Joel's trick is that $$p_0 = \min\lbrace p : \phi(0,p) \land \forall x(\phi(x,p) \to \phi(x+1,p)) \land \lnot\forall x\phi(x,p)\rbrace$$ is definable without parameters. However, the existence of $p_0$ is another instance of induction (in the guise of the least element principle). 
The complexity of a formula in arithmetic is often measured by counting the number of quantifier alternations when put into prenex form (often ignoring bounded quantifiers). With this measure, the complexity of the induction that justifies the existence of $p_0$ is strictly greater than that of the original formula $\phi(x,p)$. So there is a price to pay for removing parameters.
Therefore, when considering atithmetical theories with limited forms of induction ($EFA$, $PRA$, $IOpen$, $I\Delta_n$, $I\Sigma_n$) it is necessary to include parameters. It is also natural to think of $PA$ as the union of these restricted theories, which leads to the inclusion of parameters when formulating the induction scheme.
A: You can prove that the two theories are, in fact, equivalent. By induction (NB: 'meta-induction') on the number of parameters, we can reduce the claim to the case where you have a theory $T$ with the usual induction schema and a theory $T'$ that is an extension of $T$ by a one-parameter induction schema. 
So assume $T$ and $T'$ are not equivalent. This implies that there is a model $\mathcal{M} \vDash T'$ and a two-place open sentence $\phi(x,y)$ such that 
$$\mathcal{M} \vDash \phi(0,\beta) \wedge (\forall x (\phi(x,\beta) \rightarrow \phi(x+1,\beta))) $$ 
but  also, 
$$\mathcal{M} \nvDash \forall x \phi(x,\beta)$$
for some $\beta \in \mathcal{M}$. But note now that the above is equivalent to
$$ \mathcal{M} \vDash \exists y (\phi(0,y) \wedge (\forall z (\phi(z,y) \rightarrow \phi(z+1,y))) \wedge \neg \forall z \phi(z,y) $$
and if you call this last sentence $S$ then you get that $S \wedge \phi ' (x)$ violates the usual induction-schema, where $\phi ' (x)$ is the one-place open sentence we get by by closing $y$ under the existential quantifier in $S$. That is to say we have $S \wedge \phi ' (0)$ and $ \forall x (S \wedge \phi ' (x) \rightarrow S \wedge \phi ' (x+1))$ but not $\forall x S \wedge \phi ' (x)$. But that is a contradiction since $\mathcal{M}$ is a model of $T$. Hence the two theories are equivalent.
A: $\def\fii{\varphi}$While the other answers resolve the question, a simple way of deriving induction for a formula $\fii(x,\vec p)$ with parameters $\vec p$ is to use parameter-free induction on the formula
$$\psi(x)=\forall\vec p\,[\fii(0,\vec p)\land\forall y\,(\fii(y,\vec p)\to\fii(y+1,\vec p))\to\fii(x,\vec p)].$$
In fact, this derives the induction schema with parameters from the (parameter-free) induction rule, since $\psi(0)$ and $\psi(x)\to\psi(x+1)$ are provable in Q without any assumptions on $\fii$.
