MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
up vote 7 down vote accepted

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.

share|cite|improve this answer

$\def\fii{\varphi}$While the answers above resolve the question, I will mention that IMHO the simplest 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$.

share|cite|improve this answer
That's pretty tricky! – Marian Oct 27 '11 at 11:54
Thanks for the clear answer. I always wonder why logicians don't answer in a more formal way. This is clear positive exception. – Lucas K. Oct 27 '11 at 14:15
You’re welcome. – Emil Jeřábek Oct 27 '11 at 14:41

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.

share|cite|improve this answer

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.

share|cite|improve this answer
Are some of your $b$'s supposed to be $\beta$'s? – David Speyer Oct 26 '11 at 19:19
corrected - - - – Chuck Oct 26 '11 at 19:24

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.