# Prove the induction axiom via the induction rule

Consider the formal system $$P'$$ which is the same as $$PA$$, but without all the induction axioms and with an additional induction rule:

If $$\vdash A_x[0]$$ and $$\vdash A\to A_x[Sx]$$, then $$\vdash A$$.

Let $$A$$ be the induction axiom $$B_x[0]\wedge\forall x(B\to B_x[Sx])\to B$$ for $$B$$. I am trying to prove $$A$$ in $$P'$$. In the book it is stated as something trivial that $$A_x[0]$$ and $$A\to A_x[Sx]$$ are provable without use of induction axioms, hence $$\vdash_{P'}A$$ by the induction rule. I don't see how $$A\to A_x[Sx]$$ is provable.

Here is my approach. The deduction theorem holds in $$P'$$ since $$P'$$ has all the rules and axioms used in its proof. We have $$\vdash_{P'[B_x[0],\forall x(B\to B_x[Sx])]}B$$ by the generalization and induction rules, hence $$\vdash_{P'} A$$ by the deduction theorem. Is this approach correct?

Using your symbols, $$A$$ is $$B_x[0] ∧ ∀x(B → B_x[Sx]) → B$$.

This means that $$A_x[0]$$ will be:

$$(B_x[0] ∧ ∀x(B → B_x[Sx]) → B)_x[0]$$.

But $$x$$ does not occur free into: $$B_x[0] ∧ ∀x(B → B_x[Sx])$$ and thus $$A_x[0]$$ will be:

$$B_x[0] ∧ ∀x(B → B_x[Sx]) → B_x[0]$$.

This formula is like $$P \land Q \to P$$, which is valid, i.e. it is provable in $$P'$$ without arithmetical axioms.

In conclusion:

$$\vdash_{P'} A_x[0]$$.

The second part is a little more tricky...

We have to prove:

$$(B_x[0] ∧ ∀x(B → B_x[Sx])→B) \to (B_x[0] ∧ ∀x(B → B_x[Sx]) → B_x[Sx])$$.

Assume the antecedent: $$B_x[0] ∧ ∀x(B → B_x[Sx]) → B$$, and assume $$B_x[0] ∧ ∀x(B → B_x[Sx])$$.

By Modus Ponens: $$B$$, and using Simplification and UI we have: $$B → B_x[Sx]$$.

Using MP again: $$B_x[Sx]$$.

Now, the result follows by DT:

$$\vdash_{P'} A \to A_x[Sx]$$.

• Thank you! Since we are using the deduction theorem anyway my approach seems to be simpler, but is it correct? – Ansar Feb 24 at 8:34
• @Ansar - Yes... provided that you have the derivation $B_x[0], \forall x (B \to B_x[Sx]) \vdash_{P'} B$. As said in your book, "the result is obvious": IMO, the gist of the exercise is to write the needed derivation. – Mauro ALLEGRANZA Feb 24 at 8:54