# Complete induction in the Peano system

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$$

• My guess is that you mean $\forall _X A$ rather than $A$ at the very end of your post, right? – Apostolos Jan 25 '13 at 22:22
• Also, are you sure that axiom 7 is stated correctly? – Apostolos Jan 25 '13 at 22:29
• Well, no I did not, but your suggestion does not change much, due to universal closure and prenex normal form theorems. – superAnnoyingUser Jan 25 '13 at 22:34
• Axiom 7 is supposed to read "$\equiv$" as "iff" but I could not find the symbol. – superAnnoyingUser Jan 25 '13 at 22:35
• 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$). – 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)$.

• What do you mean by (Ho)? – superAnnoyingUser Jan 26 '13 at 12:50
• @George, $\forall x, (\forall y, y < x \Rightarrow Q(y)) \Rightarrow Q(x)$ – user58512 Jan 26 '13 at 12:50
• By Q(Y) you mean a formula that has variables among Y? – superAnnoyingUser Jan 26 '13 at 12:52
• 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.. – user58512 Jan 26 '13 at 12:56
• @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. – user58512 Jan 26 '13 at 13:11