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

Revised following Max's comments.

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 :

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

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

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

1 Answer 1


Try proving

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


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

  • $\begingroup$ Thanks, I've expanded a little bit the Question, inserting the hints; but I cannot do anything with them. $\endgroup$ Dec 23, 2013 at 20:03
  • $\begingroup$ 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))$. $\endgroup$
    – mmw
    Dec 23, 2013 at 20:43
  • $\begingroup$ 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)$. $\endgroup$
    – mmw
    Dec 23, 2013 at 20:51
  • $\begingroup$ 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)$. $\endgroup$
    – mmw
    Dec 23, 2013 at 21:02
  • $\begingroup$ Ok thanks; I'll expand the Question with the above hints. $\endgroup$ Dec 23, 2013 at 22:28

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .