Introduction to Metamathematics by S C Kleene. Help with exercise *135b needed.

Question

I'm having trouble with exercise *135b in Introduction to Metamathematics by S. C. Kleene. The ask is to show that: $\vdash 0<a^{'}$. Here is how I would do it.

Assume $a=b$. With Axiom 17 and Axiom 18 I get:

$\vdash a=b \supset b^{'}+0=a^{'}$

Assume $b^{'}+0=a^{'}$. With Axiom 18 and Axiom 14 I get:

$\vdash b^{'}+0=a^{'} \supset a=b $

Then with &$-introd.$:

$\vdash a=b \sim b^{'}+0=a^{'}$

Using *72:

$\vdash \exists b(a=b) \sim \exists b(b^{'}+0=a^{'})$

which can be abbreviated:

$\vdash \exists b(a=b) \sim 0<a^{'}$

How do I complete this? I mean, is $\vdash \exists b(a=b)$ provable? Intuitively yes, but how to formally prove it? Thanks

Answer 1

Yes, we do indeed have $\vdash\exists b(a=b)$. I don't have Kleene's book on hand, but if memory serves the following is how it plays out in Kleene's system (and most systems in general):

The relevant rule is existential introduction (or generalization). If you've deduced some formula $\varphi$, and $t$ is a term occurring in $\varphi$, then you can subsequently deduce any formula of the form $\exists x\psi(x)$ where $\psi$ is gotten from $\varphi$ by replacing some of the instances of $t$ by $x$ (and $x$ is a variable not occurring in $\varphi$ already).

The "some" there is crucial. To get $\exists b(a=b)$, we'll apply existential introduction to $a=a$ and replace the second, but not the first, instance of $a$ by $b$. So that reduces the problem to just showing $\vdash a=a$, which I believe is one of the atomic clauses in the definition of $\vdash$ in Kleene's system.