# A theorem of formal Number Theory, according to Kleene, IM (1952)

In S.C.Kleene, Introduction to Metamathematics (1952) , I've found difficulty with the proof of 148 (preliminary to least number principle) :

$\vdash \exists y[y < x \land A(y) \land \forall z( z < y \rightarrow \lnot A(z))] \lor \forall y[ y < x \rightarrow \lnot A(y)]$

The proof is :

Proof by induction on x (formula 148 is $P(x) \lor Q(x)$).

Basis: $\vdash \lnot y < 0$ ; using $\vdash \lnot A \rightarrow (A \rightarrow B )$ derive $P(0) \lor Q(0)$ by $\rightarrow$-elim, $\forall$-intro and $\lor$-intro.

Induction step: assume $P(x) \lor Q(x)$ and by cases :

 $P(x) \vdash P(x’)$, by $\land$-elim, 135a, 134a and $\land$-intro, and then $P(x’) \lor Q(x’)$, by $\lor$-intro.

 $Q(x)$ by cases with $A(x) \lor \lnot A(x)$ :

[2a] $Q(x), A(x) \vdash P(x')$ [Kleene's hint: using 135a]

We have that : $\vdash x < x′$ (by 135a), and $A(x) \vdash A(x)$, and $Q(x) \vdash \forall z (z < y \rightarrow \lnot A(z))$ (changing bound variable, by Lemma 15a).

Then $Q(x), A(x) \vdash \exists y[y < x \land A(y) \land \forall z( z < y \rightarrow \lnot A(z))]$ (by $\land$-intro and $\exists$-intro) i.e. $P(x') \vdash P(x’) \lor Q(x’)$, by $\lor$-intro.

[2b] $Q(x), \lnot A(x) \vdash Q(x')$ [Kleene's hint : using 138a]

We have that : $\vdash y < x′ \rightarrow y < x \lor y = x$, and $Q(x) \vdash y < x \rightarrow \lnot A(y)$, and $\lnot A(x) \vdash y = x \rightarrow \lnot A(y)$.

Assembling all together : $Q(x), \lnot A(x) \vdash \forall y (y < x' \lor \lnot A(y))$ (by $\forall$-intro) i.e. $Q(x') \vdash P(x’) \lor Q(x’)$, by $\lor$-intro.

• Could you please clarify how did you deduct $\lnot A(x) \vdash y=x \to \lnot A(y)$ ? Aug 19, 2020 at 16:13
• @Lorenzo; axiom for equality: substitution Aug 23, 2020 at 12:48
• Referring to Kleene's book (1952) this is Axiom 23 (§ 73, page 399) Aug 25, 2020 at 9:46

Try proving

$Q(x),A(x)\vdash P(x')$

and

$Q(x),\neg A(x)\vdash Q(x')$.

• Thanks, I've expanded a little bit the Question, inserting the hints; but I cannot do anything with them. Dec 23, 2013 at 20:03
• For $Q(x),A(x)\vdash P(x')$, note that $\vdash x<x'$, $A(x)\vdash A(x)$, and $Q(x)\vdash \forall z(z<x\to \neg A(z))$.
– mmw
Dec 23, 2013 at 20:43
• For $Q(x),\neg A(x)\vdash Q(x')$, use $\vdash y<x'\to y<x\lor y=x$, $Q(x)\vdash y<x\to \neg A(y)$ and $\neg A(x)\vdash y=x\to \neg A(y)$.
– mmw
Dec 23, 2013 at 20:51
• After all this, you have $Q(x),A(x)\vdash P(x')\lor Q(x')$ and $Q(x),\neg A(x)\vdash P(x')\lor Q(x')$. Using $\lor$-elim on these with $\vdash A(x)\lor \neg A(x)$ gives (i) $Q(x)\vdash P(x')\lor Q(x')$. We can get (ii) $P(x)\vdash P(x')\lor Q(x')$; so use $\lor$-elim on (i) and (ii) with $P(x)\lor Q(x)\vdash P(x)\lor Q(x)$.
– mmw
Dec 23, 2013 at 21:02
• Ok thanks; I'll expand the Question with the above hints. Dec 23, 2013 at 22:28