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?