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

| cite | improve this answer | |
  • $\begingroup$ Thank you! Since we are using the deduction theorem anyway my approach seems to be simpler, but is it correct? $\endgroup$ – Ansar Feb 24 at 8:34
  • $\begingroup$ @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. $\endgroup$ – Mauro ALLEGRANZA Feb 24 at 8:54

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.