Ajuda necessária com o exercício * 148 em Introdução à metamatemática de SC Kleene.

Question

Deixei $x$ ser uma variável, $A(x)$ uma fórmula e $y$ uma variável distinta de $x$ que é grátis para $x$ dentro $A(x)$ e não ocorre gratuitamente em $A(x)$.

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

Eu preciso de ajuda para provar isso $Q(x), \lnot A(x) \vdash Q(x')$ usando o sistema de Kleene (aqui está o sucessor).

Esta é a última parte do exercício * 148 (princípio do menor número para um segmento inicial dos números naturais) página 190 na Introdução de Kleene à metamatemática. De acordo com Kleene, deve ser usado:$\vdash a\le b \sim a \lt b'$

obrigado

Answer 1

Vamos usar o seguinte lema: $y < x' \rightarrow y = x \vee y < x$. Isso você pode derivar de várias maneiras: por exemplo, por meio de um argumento de indução ou simplesmente apelando para 139 e 141 estabelecidos anteriormente.

Vou dar uma prova de dedução natural de $Q(x), \neg A(x) \vdash Q(x')$. O sistema que uso pode não corresponder exatamente ao de Kleene, mas deve ser parecido o suficiente para você traduzir entre eles. Avise-me se isso lhe causar algum problema.

Já que sua conclusão desejada é $\forall y. y < x' \rightarrow \neg A(y)$, você pode começar sua prova com quatro suposições e trabalhar em direção a uma contradição.

1. Presumir $\forall y. y < x \rightarrow \neg A(y)$ - ie $Q(x)$
2. Presumir $\neg A(x)$.
3. Presumir $y < x'$.
4. Presumir $A(y)$.
5. Ter $y < x' \rightarrow y = x \vee y < x$ (pelo lema discutido acima).
6. Ter $y = x \vee y < x$ (de 5 e 1 usando eliminação de implicação).
7. Presumir $y=x$.
8. Ter $A(x)$ (de 7 e 4 usando substituição).
9. Tenha uma contradição (de 8 e 2).
10. Ter $y = x \rightarrow \neg A(y)$ (de 7-9 por contradição, descartando a suposição 7).
11. Ter $y<x \rightarrow \neg A(y)$ (de 1 por eliminação universal).
12. Ter $\neg A(y)$ (de 6, 10, 11 usando eliminação de disjunção).
13. Tem uma contradição (de 12 e 4).
14. Ter $\neg A(y)$ (de 4-13 por introdução de negação, descartando a suposição 4).
15. Ter $y < x' \rightarrow \neg A(y)$ (de 3-14 por introdução de implicação, eliminando a suposição 3).
16. Ter $\forall y. y<x' \rightarrow \neg A(y)$(de 15 por introdução universal), QED .