Is complete induction valid in the Peano model of the naturals and why. In more detail if $L$ is the first order language $\{ +, \cdot, 0, <,S\}$ and $T$ is the theory with non-logical axioms

$$PA0.\qquad 0\not= SX_0$$ $$PA1.\qquad SX_0 = SX_1 \to X_0=X_1$$ $$PA2.\qquad X_0\cdot 0=0$$ $$PA3.\qquad X_0+SX_1=S(X_0+X_1)$$ $$PA4.\qquad X_0+0=X_0$$ $$PA5.\qquad X_0\cdot SX_1=X_0\cdot X_1+X_0$$ $$PA6.\qquad X_0 \not\lt X_0$$ $$PA7.\qquad X_0 \lt SX_1\equiv X_0=X_1 \lor X_0\lt X_1$$ $$PA8.\qquad X_0 \lt X_1 \lor X_0=X_1 \lor X_1 \lt X_0$$ $$PA9.\qquad X_0 \lt X_1 \to X_1 \lt X_0 \to X_0 \lt X_2$$

In addition, the induction scheme: if A is a formula from L than for each variable X $$PA10.\qquad A_X[0]\to\forall _X(A\to A_X[SX])\to\forall _XA$$

Than show that for all formulas A, for all variables X $$\vdash \forall _X(\forall _Y(Y\lt X\to A_X[Y])\to A)\to A$$

  • $\begingroup$ My guess is that you mean $\forall _X A$ rather than $A$ at the very end of your post, right? $\endgroup$ – Apostolos Jan 25 '13 at 22:22
  • $\begingroup$ Also, are you sure that axiom 7 is stated correctly? $\endgroup$ – Apostolos Jan 25 '13 at 22:29
  • $\begingroup$ Well, no I did not, but your suggestion does not change much, due to universal closure and prenex normal form theorems. $\endgroup$ – superAnnoyingUser Jan 25 '13 at 22:34
  • $\begingroup$ Axiom 7 is supposed to read "$\equiv$" as "iff" but I could not find the symbol. $\endgroup$ – superAnnoyingUser Jan 25 '13 at 22:35
  • $\begingroup$ So $x_0<Sx_1$ if and only if $x_0=x_1$? Then you have $0<S0$ and $S0<SS0$ which implies that $0<SS0$ which implies $0=S0$. Or does your use of $x_0$ instead of $X_0$ mean something else? Or do you mean $X_0<SX_1$ if and only if $X_0=X_1\lor X_0<X_1$? I think the if-f is \leftrightarrow ($\leftrightarrow$). $\endgroup$ – Apostolos Jan 25 '13 at 22:39

Set $P(x) := \forall y, y < x \Rightarrow Q(y)$.

Given (H0) $\forall x, (\forall y, y < x \Rightarrow Q(y)) \Rightarrow Q(x)$ we use induction on $P$:

  • $\forall y, y < 0 \Rightarrow Q(0)$ trivial
  • $[\forall y, y < x \Rightarrow Q(y)] \Rightarrow [\forall y, y < Sx \Rightarrow Q(y)]$ just split the conseqent into cases (A) $y < x$ trivial by induction hypothesis (B) $y=x$ immediate from H0.

Thus we have $$[\forall x, (\forall y, y < x \Rightarrow Q(y)) \Rightarrow Q(x)] \Rightarrow \forall x, \forall y, (y < x \Rightarrow Q(y))$$ as a theorem of PA which you can now weaken to get the theorem you wanted.

We strengthened $\forall x, Q(x)$ to $\forall x, \forall y, (y < x \Rightarrow Q(y))$ to make the induction go through (this is a general technique called strengthening the induction hypothesis).

This gave us a proof of

$$(T0)\,\, [\forall x, (\forall y, y < x \Rightarrow Q(y)) \Rightarrow Q(x)] \Rightarrow \forall x, \forall y, (y < x \Rightarrow Q(y))$$

but all we really wanted was

$$(T1)\,\, [\forall x, (\forall y, y < x \Rightarrow Q(y)) \Rightarrow Q(x)] \Rightarrow \forall z, Q(z)$$

thus we use the fact that $$[\forall x, \forall y, (y < x \Rightarrow Q(y))] \Rightarrow \forall z, Q(z)$$ (to see this, set $x=Sz$, $y=z$ and use a proof of $z<Sz$) to "weaken" $(T0)$ to $(T1)$.

  • $\begingroup$ What do you mean by (Ho)? $\endgroup$ – superAnnoyingUser Jan 26 '13 at 12:50
  • $\begingroup$ @George, $\forall x, (\forall y, y < x \Rightarrow Q(y)) \Rightarrow Q(x)$ $\endgroup$ – user58512 Jan 26 '13 at 12:50
  • $\begingroup$ By Q(Y) you mean a formula that has variables among Y? $\endgroup$ – superAnnoyingUser Jan 26 '13 at 12:52
  • $\begingroup$ if $Q(x)$ was $x^2 + 1 > x$ (I can't think of any examples of things we want to prove by strong induction...) then $Q(y)$ is $y^2 + 1 > y$ and $Q(Sx)$ is $(Sx)^2 + 1 > Sx$ etc.. $\endgroup$ – user58512 Jan 26 '13 at 12:56
  • 1
    $\begingroup$ @George, the overall idea here is we want to prove H0 implies $\forall x, Q(x)$. So we try to prove $\forall x, Q(x)$ by induction with H0 as an assumption/hypothesis. But this does not work, we need to stengthen the induction hypothesis,so we try to prove $ \forall x, \forall y, (y < x \Rightarrow Q(y))$ by induction with H0 as a hypothesis. Then you weaken it to get exactly the statement of "strong induction" as a theorem in PA. $\endgroup$ – user58512 Jan 26 '13 at 13:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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