Prove the induction axiom via the induction rule

Question

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?

Answer 1

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