Predicate Logic - การหักตามธรรมชาติ
ชุดของกฎการอนุมานของการหักเงินตามธรรมชาติของ Gentzen มีความซ้ำซ้อนในแง่ที่ว่าหากไม่มีกฎของระบบมันจะยังสมบูรณ์ได้หรือไม่?
ความคิดของฉัน: ฉันเจอคำถามนี้และไม่สามารถสร้างข้อโต้แย้งที่ชัดเจนได้ว่ามีความซ้ำซ้อนในระบบหรือไม่ โปรดทราบว่าโดยเฉพาะกฎการอนุมานของการหักตามธรรมชาติของ Gentzen รวมถึง$\forall$- อินโทร, $\forall$-elim, $\exists$- อินโทร, $\exists$-elim, $\wedge$- อินโทร, $\wedge$-elim, $\lor$- อินโทร, $\lor$-elim, $\Rightarrow$- อินโทร, $\Rightarrow$-elim, $\neg$-intro และ $\neg$-elim.
คำตอบ
ไม่มีความซ้ำซ้อนเช่นนี้และนี่คือแนวคิดในการพิสูจน์
[แก้ไข: ฉันเขียนอาร์กิวเมนต์ใหม่เพื่อให้มันเข้าใจง่ายขึ้น]
ให้เรามุ่งเน้นไปที่การเชื่อมต่อ $\land$เพื่อความเรียบง่าย เอาตัวเองไปอยู่ในความคิดของคนที่ไม่รู้ว่ามีสีหน้าอย่างไร$A\land B$หมายถึง แต่ต้องการค้นหาโดยดูที่กฎการหักเงินตามธรรมชาติ วิธีหนึ่งที่คุณสามารถอ่านบทนำและกฎการกำจัดได้$\land$คือพวกเขากำหนดขอบเขตล่างและบนกับความแข็งแรงเชิงตรรกะของนิพจน์$A\land B$. ตัวอย่างเช่น,
($\land$-intro) จาก $A$ และ $B$ อนุมาน $A\land B$.
บอกคุณว่า $A\land B$มีความแข็งแกร่งมากที่สุดเท่าที่การรวมกันของ$A$ และ $B$ในขณะที่
($\land$-elim) จาก $A\land B$ อนุมาน $A$ หรือ $B$.
บอกคุณว่า $A\land B$เป็นอย่างน้อยเป็นที่แข็งแกร่งเป็นทั้ง$A$ และ $B$.
สมมติว่าตอนนี้คุณละเว้นกฎ ($\land$- อินโทร). ระบบผลลัพธ์จะบอกคุณว่าไม่มีขอบเขตบนของความแข็งแรงเชิงตรรกะของนิพจน์$A\land B$. โดยสัญชาตญาณดังนั้น$A\land B$อาจเป็นอะไรก็ได้ที่อย่างน้อยก็แข็งแกร่งพอ ๆ$A$ และ $B$. แต่ไม่มีอะไรขัดขวางคุณจากการตีความ$A\land B$ ในระบบผลลัพธ์เป็นนิพจน์ที่แข็งแกร่งที่สุด: ความขัดแย้งทางตรรกะ ($\bot$ ถ้ามีอะตอมนี้อยู่หรืออย่างอื่น $p\land\lnot p$ สำหรับตัวแปรใหม่ $p$). โปรดสังเกตว่าในการแทนที่$A\land B$ โดย $\bot$ ใน ($\land$-elim) คุณจะได้รับกฎเสียง
จาก $\bot$ อนุมาน $A$ หรือ $B$.
เป็นไปตามที่คุณไม่สามารถพิสูจน์สิ่งใดในระบบที่ขัดแย้งกับการตีความของ$A\land B$เป็นความขัดแย้ง ตัวอย่างเช่นทฤษฎีบท$q\rightarrow (q\land q)$ จะไม่สามารถพิสูจน์ได้เนื่องจาก $q\rightarrow \bot$ ไม่ถูกต้อง
ในการทำให้สัญชาตญาณนี้เป็นข้อโต้แย้งอย่างเป็นทางการให้พิจารณาคำแปล $\pi$ ซึ่งจะแทนที่ทุก subformula $A\land B$ ในสูตรโดย $\bot$. จากนั้นคุณสามารถแสดงโดยการเหนี่ยวนำกับความยาวพิสูจน์ว่าถ้าเป็นสูตร$F$ สามารถพิสูจน์ได้ใน Natural Deduction โดยไม่มีกฎ ($\land$-intro) แล้ว $\pi(F)$ สามารถพิสูจน์ได้ในการหักตามธรรมชาติโดยไม่ ($\land$-intro) ด้วย. มันเป็นไปตามทฤษฎีบทนั้น$q\rightarrow (q\land q)$ ไม่สามารถพิสูจน์ได้หากไม่มี ($\land$-intro) ก็จะเป็นเช่นนั้น $\pi(q\rightarrow (q\land q))=q\rightarrow \bot$ซึ่งไม่ถูกต้อง ดังนั้นการหักตามธรรมชาติโดยไม่ ($\land$-intro) ไม่สมบูรณ์
สามารถพบอาร์กิวเมนต์ที่คล้ายกันสำหรับการละเว้นกฎอื่น ๆ