Bantuan yang dibutuhkan dengan latihan * 148 di SC Kleene Pengantar metamathematics.

Question

Membiarkan $x$ menjadi variabel, $A(x)$ rumus dan $y$ variabel yang berbeda dari $x$ yang gratis untuk $x$ di $A(x)$ dan tidak terjadi gratis di $A(x)$.

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

Saya butuh bantuan untuk membuktikannya $Q(x), \lnot A(x) \vdash Q(x')$ menggunakan sistem Kleene (di sini 'adalah penerusnya).

Ini adalah bagian terakhir dari latihan * 148 (prinsip bilangan terkecil untuk segmen awal bilangan asli) halaman 190 di Kleene's Introduction to metamathematics. Menurut Kleene ini harus digunakan:$\vdash a\le b \sim a \lt b'$

Terima kasih

Answer 1

Kami akan menggunakan lemma berikut: $y < x' \rightarrow y = x \vee y < x$. Ini dapat Anda peroleh dengan beberapa cara: misalnya melalui argumen induksi, atau hanya dengan mengajukan banding ke 139 dan 141 yang ditetapkan sebelumnya.

Saya akan memberikan bukti deduksi alami $Q(x), \neg A(x) \vdash Q(x')$. Sistem yang saya gunakan mungkin tidak sama persis dengan Kleene, tetapi harus cukup mirip sehingga Anda dapat menerjemahkannya. Beri tahu saya jika itu membuat Anda kesulitan.

Karena kesimpulan yang Anda inginkan adalah $\forall y. y < x' \rightarrow \neg A(y)$, Anda dapat memulai pembuktian dengan empat asumsi dan bekerja menuju kontradiksi.

1. Menganggap $\forall y. y < x \rightarrow \neg A(y)$ - mis $Q(x)$
2. Menganggap $\neg A(x)$.
3. Menganggap $y < x'$.
4. Menganggap $A(y)$.
5. Memiliki $y < x' \rightarrow y = x \vee y < x$ (oleh lemma dibahas di atas).
6. Memiliki $y = x \vee y < x$ (dari 5 dan 1 menggunakan eliminasi implikasi).
7. Menganggap $y=x$.
8. Memiliki $A(x)$ (dari 7 dan 4 menggunakan substitusi).
9. Memiliki kontradiksi (dari 8 dan 2).
10. Memiliki $y = x \rightarrow \neg A(y)$ (dari 7-9 oleh kontradiksi, pemakaian asumsi 7).
11. Memiliki $y<x \rightarrow \neg A(y)$ (dari 1 dengan eliminasi universal).
12. Memiliki $\neg A(y)$ (dari 6, 10, 11 menggunakan eliminasi disjungsi).
13. Memiliki kontradiksi (dari 12 dan 4).
14. Memiliki $\neg A(y)$ (dari 4-13 dengan pengenalan negasi, asumsi pemakaian 4).
15. Memiliki $y < x' \rightarrow \neg A(y)$ (dari 3-14 dengan pengenalan implikasi, asumsi pemakaian 3).
16. Memiliki $\forall y. y<x' \rightarrow \neg A(y)$(dari 15 dengan pengantar universal), QED .