Aide nécessaire avec l'exercice * 148 dans SC Kleene Introduction aux métamathématiques.

Question

Laisser $x$ être une variable, $A(x)$ une formule et $y$ une variable distincte de $x$ qui est gratuit pour $x$ dans $A(x)$ et ne se produit pas gratuitement dans $A(x)$.

Laisser $Q(x)$ être: $\forall y [y<x \Rightarrow \lnot A(y)]$.

J'ai besoin d'aide pour prouver que $Q(x), \lnot A(x) \vdash Q(x')$ en utilisant le système de Kleene (voici le successeur).

Ceci est le dernier exercice * 148 (principe du moindre nombre pour un segment initial des nombres naturels) page 190 dans l'introduction de Kleene aux métamathématiques. Selon Kleene, cela devrait être utilisé:$\vdash a\le b \sim a \lt b'$

Merci

Answer 1

Nous allons utiliser le lemme suivant: $y < x' \rightarrow y = x \vee y < x$. Vous pouvez en déduire cela de plusieurs manières: par exemple via un argument d'induction, ou simplement en faisant appel aux 139 et 141 établis précédemment.

Je donnerai une preuve de déduction naturelle de $Q(x), \neg A(x) \vdash Q(x')$. Le système que j'utilise peut ne pas correspondre exactement à celui de Kleene, mais devrait lui ressembler suffisamment pour que vous puissiez traduire entre eux. Faites-moi savoir si cela vous pose des problèmes.

Puisque votre conclusion souhaitée est $\forall y. y < x' \rightarrow \neg A(y)$, vous pouvez commencer votre preuve avec quatre hypothèses et travailler vers une contradiction.

1. Présumer $\forall y. y < x \rightarrow \neg A(y)$ - c'est à dire $Q(x)$
2. Présumer $\neg A(x)$.
3. Présumer $y < x'$.
4. Présumer $A(y)$.
5. Avoir $y < x' \rightarrow y = x \vee y < x$ (par le lemme discuté ci-dessus).
6. Avoir $y = x \vee y < x$ (de 5 à 1 en utilisant l'élimination d'implication).
7. Présumer $y=x$.
8. Avoir $A(x)$ (de 7 et 4 en utilisant la substitution).
9. Avoir une contradiction (de 8 et 2).
10. Avoir $y = x \rightarrow \neg A(y)$ (de 7-9 par contradiction, décharge de l'hypothèse 7).
11. Avoir $y<x \rightarrow \neg A(y)$ (de 1 par élimination universelle).
12. Avoir $\neg A(y)$ (de 6, 10, 11 en utilisant l'élimination de disjonction).
13. Avoir une contradiction (de 12 et 4).
14. Avoir $\neg A(y)$ (de 4 à 13 par introduction de négation, décharge de l'hypothèse 4).
15. Avoir $y < x' \rightarrow \neg A(y)$ (de 3 à 14 par introduction implicite, décharge de l'hypothèse 3).
16. Avoir $\forall y. y<x' \rightarrow \neg A(y)$(à partir de 15 par introduction universelle), QED .