Let $x$ be a variable, $A(x)$ a formula and $y$ a variable distinct from $x$ which is free for $x$ in $A(x)$ and does not occur free in $A(x)$.

Let $Q(x)$ be: $\forall y [y<x \Rightarrow \lnot A(y)]$.

I need some help in proving that $Q(x), \lnot A(x) \vdash Q(x')$ using Kleene's system (here ' is the successor).

This is the last bit of exercise *148 (least number principle for an initial segment of the natural numbers) page 190 in Kleene's Introduction to metamathematics. According to Kleene this should be used: $\vdash a\le b \sim a \lt b'$



We are going to use the following lemma: $y < x' \rightarrow y = x \vee y < x$. This you can derive in several ways: e.g. via an induction argument, or simply by appealing to 139 and 141 established earlier.

I'll give a natural deduction proof of $Q(x), \neg A(x) \vdash Q(x')$. The system I use might not correspond exactly to Kleene's, but should resemble it enough for you to translate between them. Let me know if that gives you any trouble.

Since your desired conclusion is $\forall y. y < x' \rightarrow \neg A(y)$, you can start off your proof with four assumptions and work toward a contradiction.

  1. Assume $\forall y. y < x \rightarrow \neg A(y)$ - i.e. $Q(x)$
  2. Assume $\neg A(x)$.
  3. Assume $y < x'$.
  4. Assume $A(y)$.
  5. Have $y < x' \rightarrow y = x \vee y < x$ (by the lemma discussed above).
  6. Have $y = x \vee y < x$ (from 5 and 1 using implication elimination).
  7. Assume $y=x$.
  8. Have $A(x)$ (from 7 and 4 using substitution).
  9. Have a contradiction (from 8 and 2).
  10. Have $y = x \rightarrow \neg A(y)$ (from 7-9 by contradiction, discharging assumption 7).
  11. Have $y<x \rightarrow \neg A(y)$ (from 1 by universal elimination).
  12. Have $\neg A(y)$ (from 6, 10, 11 using disjunction elimination).
  13. Have a contradiction (from 12 and 4).
  14. Have $\neg A(y)$ (from 4-13 by negation introduction, discharging assumption 4).
  15. Have $y < x' \rightarrow \neg A(y)$ (from 3-14 by implication introduction, discharging assumption 3).
  16. Have $\forall y. y<x' \rightarrow \neg A(y)$ (from 15 by universal introduction), QED.
  • $\begingroup$ It's not clear how to translate step 8. In Kleene's IM (1952) if $x$ is a variable, $A(x)$ is a formula, and t is a term which is free for $x$ in $A(x)$: $A(x) \vdash^x A(t)$. The variable "$x$" written as a superscript on the symbol $\vdash$ is to mark an application of Rule 9 or 12 with respect to $x$ in constructing the resulting deduction. For the predicate calculus (or the full number-theoretic system), all the rules hold (e.g. negation introduction), provided that in each subsidiary deduction the free variables are held constant for the assumption to be discharged. $\endgroup$ – Lorenzo Aug 20 '20 at 15:07
  • $\begingroup$ Assuning A(y): A(y)⊢yA(x). By weak ¬−elim: A(x),¬A(x)⊢y=x→¬A(y). By ∨−elim: y=x∨y<x,y=x→¬A(y),y<x→¬A(y)⊢¬A(y). This can be written as: y=x∨y<x,A(y),¬A(x),Q(x)⊢y¬A(y). By general properties of ⊢: y=x∨y<x,¬A(y),¬A(x),Q(x)⊢¬A(y). If we could use ¬−introd: y=x∨y<x,¬A(x),Q(x)⊢¬A(y), but we can't because the y in the assumption A(y) in one of the subsidiary deductions is not held constant. $\endgroup$ – Lorenzo Aug 20 '20 at 15:07
  • $\begingroup$ As far as I can see neither Rule 9 nor Rule 12 are applied at all in that particular subsidiary deduction, so I don't see how anything varies, and how the restrictions of section 32(3) would apply. Then again, I don't use Kleene's system, so you should wait for someone who does to clarify this. You could try asking a follow-up question about deriving $\varphi(x),x=y \vdash \varphi(y)$ in Kleene's system to speed up that process. $\endgroup$ – Z. A. K. Aug 20 '20 at 19:04

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.