ความช่วยเหลือที่จำเป็นในการออกกำลังกาย * 148 ใน SC Kleene Introduction to metamathematics

Question

ปล่อย $x$ เป็นตัวแปร $A(x)$ สูตรและ $y$ ตัวแปรที่แตกต่างจาก $x$ ซึ่งฟรีสำหรับ $x$ ใน $A(x)$ และไม่เกิดขึ้นฟรีใน $A(x)$.

ปล่อย $Q(x)$ เป็น: $\forall y [y<x \Rightarrow \lnot A(y)]$.

ฉันต้องการความช่วยเหลือในการพิสูจน์ว่า $Q(x), \lnot A(x) \vdash Q(x')$ โดยใช้ระบบของคลีน (นี่คือตัวตายตัวแทน)

นี่คือส่วนสุดท้ายของแบบฝึกหัด * 148 (หลักการจำนวนน้อยที่สุดสำหรับส่วนเริ่มต้นของจำนวนธรรมชาติ) หน้า 190 ในบทนำเกี่ยวกับอภิคณิตศาสตร์ของคลีน ตามที่ Kleene ควรใช้:$\vdash a\le b \sim a \lt b'$

ขอบคุณ

Answer 1

เราจะใช้คำนามต่อไปนี้: $y < x' \rightarrow y = x \vee y < x$. สิ่งนี้คุณสามารถได้มาจากหลายวิธีเช่นผ่านอาร์กิวเมนต์แบบอุปนัยหรือเพียงแค่ดึงดูด 139 และ 141 ที่สร้างขึ้นก่อนหน้านี้

ฉันจะให้หลักฐานการหักตามธรรมชาติของ $Q(x), \neg A(x) \vdash Q(x')$. ระบบที่ฉันใช้อาจไม่ตรงกับของคลีนทุกประการ แต่ควรมีลักษณะคล้ายกันมากพอที่คุณจะแปลได้ โปรดแจ้งให้เราทราบหากคุณมีปัญหา

เนื่องจากข้อสรุปที่คุณต้องการคือ $\forall y. y < x' \rightarrow \neg A(y)$คุณสามารถเริ่มต้นจากการพิสูจน์ของคุณด้วยสมมติฐานสี่ข้อและพยายามหาข้อขัดแย้ง

1. สมมติ $\forall y. y < x \rightarrow \neg A(y)$ - เช่น $Q(x)$
2. สมมติ $\neg A(x)$.
3. สมมติ $y < x'$.
4. สมมติ $A(y)$.
5. มี $y < x' \rightarrow y = x \vee y < x$ (ตามคำนามที่กล่าวถึงข้างต้น)
6. มี $y = x \vee y < x$ (จาก 5 และ 1 โดยใช้การกำจัดนัย)
7. สมมติ $y=x$.
8. มี $A(x)$ (จาก 7 และ 4 โดยใช้การเปลี่ยนตัว)
9. มีความขัดแย้ง (จาก 8 และ 2)
10. มี $y = x \rightarrow \neg A(y)$ (จาก 7-9 โดยความขัดแย้งการปลดปล่อยสมมติฐาน 7)
11. มี $y<x \rightarrow \neg A(y)$ (จาก 1 โดยการกำจัดสากล)
12. มี $\neg A(y)$ (จาก 6, 10, 11 โดยใช้การตัดการแยกส่วน)
13. มีความขัดแย้ง (จาก 12 และ 4)
14. มี $\neg A(y)$ (จาก 4-13 โดยการแนะนำการปฏิเสธการปล่อยสมมติฐาน 4)
15. มี $y < x' \rightarrow \neg A(y)$ (จาก 3-14 โดยการแนะนำโดยนัยการปลดปล่อยสมมติฐาน 3)
16. มี $\forall y. y<x' \rightarrow \neg A(y)$(ตั้งแต่วันที่ 15 โดยการแนะนำสากล) QED