ทฤษฎีบทการหัก - การตีความ
ในหนังสือ "A tour through mathematical logic" - โดย Robert S. Wolf ได้ระบุทฤษฎีบทการหักไว้ดังนี้:
ถ้า T $\cup$ {P} $\vdash$ Q แล้ว T $\vdash$ (ป $\to$ Q)
โดยที่ T เป็นทฤษฎีลำดับที่หนึ่งและ P & Q คือสูตรบางอย่างในภาษาของทฤษฎีลำดับที่หนึ่งนี้ แล้วการตีความทฤษฎีบท - ทฤษฎีบทต่อไปนี้ถูกต้องหรือไม่?
ถ้า Q ได้มา / พิสูจน์ได้จาก T $\cup$ {P} เราสามารถพูดได้ว่า - ถ้า P เป็นที่มาจาก T (เช่น P คือทฤษฎีบทของ T) ดังนั้น Q ก็มาจาก T เช่นกัน
นอกจากนี้การตีความนี้จับสาระสำคัญของทฤษฎีบทการหักได้หรือไม่?
ป.ล. :คำถามอื่นที่ชื่อว่าทฤษฎีการหักล้าง - สัญชาตญาณดูเหมือนจะมุ่งเน้นไปที่แง่มุมทางวากยสัมพันธ์ของทฤษฎีบทและแคลคูลัสเพรดิเคตโดยทั่วไป - แทนที่จะเป็นความหมาย
คำตอบ
การตีความทฤษฎีบท - ทฤษฎีบทต่อไปนี้ถูกต้องหรือไม่?
ไม่สิ่งที่คุณเขียนคือ
ถ้า $T \cup \{P\} \vdash Q$แล้วถ้า $T \vdash P$แล้ว $T \vdash Q$.
นี่ก็เหมือนกับที่พูด
(1) ถ้า $T \cup \{P\} \vdash Q$แล้ว $T \nvdash P$ หรือ $T \vdash Q$.
แต่สิ่งนี้ไม่เทียบเท่ากับ
(2) ถ้า $T \cup \{P\} \vdash Q$แล้ว $T \vdash P \to Q$.
ก็อาจจะเป็นอย่างนั้น $P$ ไม่สามารถพิสูจน์ได้ แต่ $P \to Q$ไม่ใช่อย่างใดอย่างหนึ่ง แล้ว "$T \nvdash P$ หรือ $T \vdash Q$"ถือ แต่"$T \vdash P \to Q$"ไม่ดังนั้น (1) $\not \Rightarrow$ (2).
นี่คือความหมายในความคิดเห็นโดย "trivialization": "if $T \vdash P$ แล้ว $T \vdash Q$"(= สิ่งที่คุณเขียน) กลายเป็นจริงเล็กน้อยถ้า $T \nvdash P$กล่าวคือถ้า $P$ไม่สามารถพิสูจน์ได้ แต่ "$T \vdash P \to Q$"(= สิ่งที่ทฤษฎีบทระบุว่า) ไม่ได้: เพียงเพราะเราพิสูจน์ไม่ได้ $P$ ไม่ได้หมายความว่าเราสามารถพิสูจน์ได้ $P\to Q$- ตามที่คุณสังเกต ด้วยเหตุนี้ "$T \vdash P \to Q$"เป็นคำกล่าวอ้างที่แข็งแกร่งกว่า" ถ้า $T \vdash P$ แล้ว $T \vdash Q$".
สาระสำคัญของทฤษฎีบทการหักมุมคือคุณสามารถ "flip-flop" ระหว่างการมีทฤษฎีบทที่ขึ้นอยู่กับสมมติฐานแบบเปิดและการพิสูจน์คำสั่งเงื่อนไข:
หากมีการพิสูจน์$Q$ ซึ่งยังคงขึ้นอยู่กับสมมติฐาน $P$จากนั้นจะมีการพิสูจน์ในทฤษฎีของคำสั่ง $P \to Q$. นี่เป็นผลทันทีของเทคนิคการพิสูจน์เงื่อนไข (ดูหน้า 14)
และสำหรับทิศทางการสนทนาของทฤษฎีบทการหักถ้าคุณสามารถพิสูจน์ได้$P \to Q$แล้วคุณจะสามารถพิสูจน์ได้ $Q$ ภายใต้สมมติฐานที่ว่า $P$. นี่คือผลของวิธีการทำงาน ponensกฎของการอนุมาน (ดูพี. 13)
ทั้งสองทิศทางรวมกันทฤษฎีบทการหักจะแสดงให้เห็นว่าเราหมายถึงอะไรโดยมีหลักฐานว่า "$\to$".
คุณมีสิทธิอย่างสมบูรณ์ในการชี้ให้เห็นว่าแนวคิดหลักของระบบที่เป็นทางการคือการพิสูจน์มากกว่าความจริง แต่โปรดทราบว่าโดยปกติแล้วเราสนใจที่จะออกแบบระบบการพิสูจน์ "ที่เป็นประโยชน์" ซึ่ง "สอดคล้อง" กับแนวคิดเรื่องความจริง: คำสั่งควรพิสูจน์ได้ในทฤษฎีอย่างแน่นอนเมื่อเป็นจริงในทุกแบบจำลองของทฤษฎี . ท้ายที่สุดแล้วประเด็นของระบบการพิสูจน์คือการมีเครื่องจักรกลเพื่อพิสูจน์ข้อความที่เราพิจารณาว่าเป็นความจริงอย่างเข้มงวด ดังนั้นในขณะที่แนวคิดของการพิสูจน์$\to$ ถูกกำหนดขึ้นในแง่ของกฎการอนุมานวิธีที่ใช้กฎเหล่านี้สะท้อนถึงตารางความจริงสำหรับ $\to$: ระบบการพิสูจน์ควรเป็น (และสำหรับระบบการพิสูจน์ที่นำเสนอในหนังสือของวูล์ฟคือ) เสียงเขียนความหมาย: สิ่งที่พิสูจน์ได้ว่าเป็นจริง (ตามนิยามตารางความจริง) ในโครงสร้างทั้งหมด ระบบ (หวังว่า) จะไม่พิสูจน์เรื่องไร้สาระแบบสุ่ม