ในตรรกศาสตร์และทฤษฎีการ พิสูจน์ การอนุมานแบบธรรมชาติ เป็น แคลคูลัสการพิสูจน์ชนิดหนึ่งซึ่งการให้เหตุผลเชิงตรรกะแสดงออกโดยกฎการอนุมานที่เกี่ยวข้องอย่างใกล้ชิดกับวิธีการให้เหตุผลแบบ "ธรรมชาติ" ^{[ 1 ]}ซึ่งแตกต่างจากระบบแบบฮิลเบิร์ตซึ่งใช้สัจพจน์ให้มากที่สุดเท่าที่จะเป็นไปได้เพื่อแสดงกฎตรรกะของการให้เหตุผลแบบนิรนัย

การอนุมานแบบธรรมชาติเกิดขึ้นจากบริบทของความไม่พอใจต่อระบบสัจพจน์ของการให้เหตุผลแบบนิรนัยที่พบได้ทั่วไปในระบบของฮิลเบิร์ตเฟรเกและรัสเซล (ดูเช่นระบบฮิลเบิร์ต ) ระบบสัจพจน์ดังกล่าวถูกใช้โดยรัสเซลและไวท์เฮด อย่างโด่งดังที่สุด ในตำราคณิตศาสตร์Principia Mathematica ของพวกเขา แรงกระตุ้นจากชุดสัมมนาในโปแลนด์ในปี 1926 โดยลูคาซิวิชที่สนับสนุนการจัดการตรรกะแบบธรรมชาติมากขึ้น ทำให้ ยาสโกวสกีพยายามกำหนดนิยามการอนุมานแบบธรรมชาติมากขึ้นเป็นครั้งแรกในปี 1929 โดยใช้สัญกรณ์แผนภาพ และต่อมาได้ปรับปรุงข้อเสนอของเขาในชุดบทความในปี 1934 และ 1935 ^{[ 2 ]}ข้อเสนอของเขานำไปสู่สัญกรณ์ที่แตกต่างกัน เช่นสัญกรณ์ฟิตช์หรือ วิธีของ ซัปเปสซึ่งเลมมอนได้ให้รูปแบบที่รู้จักกันในปัจจุบันว่าสัญกรณ์ซัปเปส-เลมมอน

การอนุมานเชิงธรรมชาติในรูปแบบสมัยใหม่ได้รับการเสนอโดยอิสระโดยนักคณิตศาสตร์ชาวเยอรมันGerhard Gentzenในปี 1933 ในวิทยานิพนธ์ที่ส่งให้กับคณะวิทยาศาสตร์คณิตศาสตร์ของมหาวิทยาลัย Göttingen [ ^{3 ] คำ}ว่าการอนุมานเชิงธรรมชาติ (หรือที่จริงแล้ว คำที่เทียบเท่าในภาษาเยอรมันคือnatürliches Schließen ) ได้รับการบัญญัติขึ้นในเอกสารฉบับนั้น:

เกนท์เซนได้รับแรงบันดาลใจจากความปรารถนาที่จะสร้างความสอดคล้องของทฤษฎีจำนวนเขาไม่สามารถพิสูจน์ผลลัพธ์หลักที่จำเป็นสำหรับผลลัพธ์ความสอดคล้อง ซึ่งก็คือทฤษฎีบทการกำจัดการตัด —Hauptsatz—โดยตรงสำหรับการอนุมานตามธรรมชาติ ด้วยเหตุนี้ เขาจึงแนะนำระบบทางเลือกของเขา คือแคลคูลัสลำดับซึ่งเขาได้พิสูจน์ Hauptsatz ทั้งสำหรับตรรกะแบบคลาสสิกและ แบบสัญชาตญาณ ในชุดสัมมนาในปี 1961 และ 1962 พราวิตซ์ได้สรุปแคลคูลัสการอนุมานตามธรรมชาติอย่างครอบคลุม และนำงานของเกนท์เซนเกี่ยวกับแคลคูลัสลำดับส่วนใหญ่มาใช้ในกรอบการอนุมานตามธรรมชาติ หนังสือโมโนกราฟของเขาในปี 1965 เรื่องNatural deduction: a proof-theoretical study ^{[ 5 ]}กลายเป็นงานอ้างอิงเกี่ยวกับการอนุมานตามธรรมชาติ และรวมถึงการประยุกต์ใช้สำหรับ ตรรกะ เชิงโมดอลและลำดับที่สอง

ในการอนุมานแบบธรรมชาติข้อเสนอจะถูกอนุมานจากชุดของข้อตั้งต้นโดยการใช้กฎการอนุมานซ้ำ ๆ ระบบที่นำเสนอในบทความนี้เป็นรูปแบบเล็กน้อยของสูตรของ Gentzen หรือ Prawitz แต่ยึดตามคำอธิบายของMartin-Löf เกี่ยวกับการตัดสินเชิงตรรกะและตัวเชื่อมอย่างใกล้ชิดยิ่งขึ้น ^{[ 6 ]}

การอนุมานตามธรรมชาติมีรูปแบบการเขียนสัญลักษณ์ที่หลากหลาย^{[ 7 ]}ซึ่งอาจทำให้ผู้อ่านที่ไม่คุ้นเคยกับรูปแบบใดรูปแบบหนึ่งจดจำการพิสูจน์ได้ยาก เพื่อช่วยในสถานการณ์นี้ บทความนี้มี ส่วน § สัญลักษณ์ที่อธิบายวิธีการอ่านสัญลักษณ์ทั้งหมดที่จะใช้จริง ส่วนนี้จะอธิบายเพียงวิวัฒนาการทางประวัติศาสตร์ของรูปแบบการเขียนสัญลักษณ์ ซึ่งส่วนใหญ่ไม่สามารถแสดงได้เนื่องจากไม่มีภาพประกอบที่ได้รับอนุญาตภายใต้ลิขสิทธิ์สาธารณะ – ผู้อ่านสามารถดูภาพประกอบ ได้ที่ SEPและIEP

• เกนท์เซนคิดค้นการอนุมานเชิงธรรมชาติโดยใช้การพิสูจน์แบบต้นไม้ – ดูรายละเอียดเพิ่มเติมได้ที่หัวข้อ§ สัญลักษณ์ต้นไม้ของเกนท์เซน
• Jaśkowskiเปลี่ยนสิ่งนี้เป็นสัญกรณ์ที่ใช้กล่องซ้อนกันหลายชั้น^{[ 7 ]}
• Fitchเปลี่ยนวิธีการวาดกล่องของ Jaśkowski ทำให้เกิดสัญกรณ์ Fitchขึ้น^{[ 7 ]}
• พ.ศ. 2483: ในตำราเรียนQuine ^{[ 8 ]}ระบุการพึ่งพาของสิ่งก่อนหน้าโดยใช้หมายเลขบรรทัดในวงเล็บเหลี่ยม ซึ่งเป็นการคาดการณ์ถึงสัญกรณ์หมายเลขบรรทัดของ Suppes ในปี พ.ศ. 2490
• ปี 1950: ในตำราเรียนเล่มหนึ่งQuine (1982 , หน้า 241–255) ได้สาธิตวิธีการใช้เครื่องหมายดอกจันหนึ่งตัวหรือมากกว่านั้นทางด้านซ้ายของแต่ละบรรทัดของการพิสูจน์เพื่อระบุความสัมพันธ์เชิงตรรกะ ซึ่งเทียบเท่ากับเครื่องหมายขีดแนวตั้งของ Kleene (ไม่แน่ชัดนักว่าสัญลักษณ์ดอกจันของ Quine ปรากฏในฉบับพิมพ์ครั้งแรกปี 1950 หรือถูกเพิ่มเข้ามาในฉบับพิมพ์ภายหลัง)
• ปี 1957: บทนำเกี่ยวกับการพิสูจน์ทฤษฎีบทตรรกศาสตร์เชิงปฏิบัติในตำราเรียนโดยSuppes (1999 , หน้า 25–150) ซึ่งระบุความสัมพันธ์ (เช่น ข้อเสนอที่เป็นเงื่อนไข) โดยใช้หมายเลขบรรทัดทางด้านซ้ายของแต่ละบรรทัด
• 1963: Stoll (1979 , หน้า 183–190, 215–219) ใช้ชุดหมายเลขบรรทัดเพื่อระบุความสัมพันธ์ของบรรทัดข้อโต้แย้งเชิงตรรกะตามลำดับโดยอาศัยกฎการอนุมานแบบหักล้างตามธรรมชาติ
• ปี 1965: ตำราเรียนฉบับสมบูรณ์ของเลมมอน (1978)เป็นบทนำเกี่ยวกับการพิสูจน์ทางตรรกศาสตร์โดยใช้วิธีการที่อิงตามวิธีการของซัปเปสซึ่งปัจจุบันรู้จักกันในชื่อสัญกรณ์ซัปเปส-เลมมอน
• 1967: ในตำราเรียนKleene (2002 , หน้า 50–58, 128–130) ได้สาธิตการพิสูจน์ตรรกะเชิงปฏิบัติสองประเภทโดยสังเขป ระบบหนึ่งใช้การอ้างอิงข้อเสนอก่อนหน้าอย่างชัดเจนทางด้านซ้ายของแต่ละบรรทัด อีกระบบหนึ่งใช้เส้นแบ่งแนวตั้งทางด้านซ้ายเพื่อระบุความสัมพันธ์^{[ 9 ]}

ตารางต่อไปนี้แสดงรูปแบบการเขียนตัวเชื่อมตรรกะที่ใช้ กันทั่วไปมากที่สุด

รูปแบบการเขียนของตัวเชื่อม^{[ 10 ] [ 11 ]}

การเชื่อมต่อ	เครื่องหมาย
และ	${\displaystyle A\land B}$, , , ,${\displaystyle A\cdot B}$${\displaystyle AB}$${\displaystyle A\mathbin {\&} B}$${\displaystyle A\mathbin {\&\&} B}$
เทียบเท่า	${\displaystyle A\equiv B}$, , ,${\displaystyle A\ลูกศรซ้าย B}$${\displaystyle A\ลูกศรขวา B}$${\displaystyle A\leftrightharpoons B}$
หมายความว่า	${\displaystyle A\Rightarrow B}$, ,${\displaystyle A\supset B}$${\displaystyle A\rightarrow B}$
เอ็นแอนด์	${\displaystyle A\mathbin {\overline {\land }} B}$, ,${\displaystyle A\mid B}$${\displaystyle {\overline {A\cdot B}}}$
ไม่เทียบเท่า	${\displaystyle A\not \equiv B}$, ,${\displaystyle A\not \Leftrightarrow B}$${\displaystyle A\nleftrightarrow B}$
ก็ไม่เช่นกัน	${\displaystyle A\mathbin {\overline {\lor }} B}$, ,${\displaystyle A\mathbin {\downarrow } B}$${\displaystyle {\overline {A+B}}}$
ไม่	${\displaystyle \neg A}$, , ,${\displaystyle -A}$${\displaystyle {\overline {A}}}$${\displaystyle {\mathord {\sim }}A}$
หรือ	${\displaystyle A\lor B}$, , ,${\displaystyle A+B}$${\displaystyle A\mid B}$${\displaystyle A\parallel B}$
เอ็กซ์เอ็นอาร์	${\displaystyle A\mathbin {\textsf {XNOR}} B}$
เอ็กซ์ออร์	${\displaystyle A\mathbin {\underline {\lor }} B}$,${\displaystyle A\oplus B}$

เกนท์เซนผู้คิดค้นการอนุมานเชิงธรรมชาติ มีรูปแบบการเขียนสัญลักษณ์เฉพาะตัวสำหรับการให้เหตุผล ซึ่งจะยกตัวอย่างโดยใช้การให้เหตุผลอย่างง่ายต่อไปนี้ สมมติว่าเรามีตัวอย่างการให้เหตุผลอย่างง่ายในตรรกศาสตร์เชิงประพจน์เช่น "ถ้าฝนตกแล้วท้องฟ้ามีเมฆมาก ฝนตกอยู่ ดังนั้นท้องฟ้าจึงมีเมฆมาก" (นี่คือการ ให้ เหตุผลแบบ modus ponens ) หากแสดงสิ่งนี้เป็นรายการของประพจน์ ดังที่นิยมใช้ เราจะได้:

${\displaystyle 1)~P\to Q}$

${\displaystyle 2)~P}$

${\displaystyle \therefore ~Q}$

ในสัญลักษณ์ของ Gentzen ^{[ 7 ]}จะเขียนได้ดังนี้:

${\displaystyle {\frac {P\to Q,P}{Q}}}$

ข้อสมมติจะแสดงอยู่เหนือเส้นที่เรียกว่าเส้นอนุมาน^{[ 12 ] [ 13 ]}คั่นด้วยเครื่องหมายจุลภาคซึ่งบ่งชี้ถึงการรวมกันของข้อสมมติ^{[ 14 ]}ข้อสรุปจะเขียนไว้ใต้เส้นอนุมาน^{[ 12 ]}เส้นอนุมานแสดงถึงผลลัพธ์ทางไวยากรณ์ [ ^{12 ]}บางครั้งเรียกว่าผลลัพธ์แบบนิรนัย^{[ 15 ] [ 16 ]}ซึ่งมีสัญลักษณ์เป็น ⊢ ^{[ 16 ]}ดังนั้นข้างต้นจึงสามารถเขียนได้ในบรรทัดเดียวเช่นกัน(สัญลักษณ์ ⊢ สำหรับผลลัพธ์ทางไวยากรณ์มีลำดับความสำคัญ ต่ำกว่าเครื่องหมายจุลภาค ซึ่งแสดงถึงการรวมกัน ^ของข้อสมมติ ซึ่งมีลำดับความสำคัญต่ำกว่าลูกศรที่ใช้สำหรับนัยยะเชิงเนื้อหา ดังนั้นจึงไม่จำเป็นต้องใช้วงเล็บในการตีความสูตรนี้) ^{[ 14 ]}${\displaystyle P\to Q,P\vdash Q}$

ผลที่ตามมาทางไวยากรณ์จะแตกต่างจากผลที่ตามมาทางความหมาย [ ^{17 ]}ซึ่งใช้สัญลักษณ์ ⊧ ^{[ 18 ] [ 16 ]}ในกรณีนี้ ข้อสรุปจะตามมาทางไวยากรณ์เนื่องจากการอนุมานตามธรรมชาติเป็น^ระบบการพิสูจน์ทางไวยากรณ์ซึ่งถือว่ากฎการอนุมานเป็นพื้นฐาน

บทความนี้จะใช้รูปแบบของเกนท์เซนเป็นส่วนใหญ่ เราสามารถหลีกเลี่ยงการใช้คำอธิบายประกอบแบบปลดปล่อยของเกนท์เซนเพื่อสรุปการตัดสินเชิงสมมติฐานได้โดยการแสดงการพิสูจน์เป็นแผนผังลำดับΓ ⊢  A  แทนที่จะเป็นแผนผังการตัดสินว่าA (เป็นจริง)

ตำราเรียนหลายเล่มใช้สัญกรณ์ Suppes–Lemmon [ ^{7 ]}ดังนั้นบทความนี้จึงจะใช้สัญกรณ์นั้นด้วย แม้ว่าในขณะนี้จะรวมเฉพาะตรรกศาสตร์เชิงประพจน์^{เท่านั้น}และส่วนที่เหลือจะครอบคลุมเฉพาะในรูปแบบ Gentzen เท่านั้น การพิสูจน์ที่จัดทำขึ้นตาม รูปแบบ สัญกรณ์ Suppes–Lemmonคือลำดับของบรรทัดที่มีประโยค^{[ 19 ]}โดยแต่ละประโยคเป็นได้ทั้งข้อสมมติ หรือผลลัพธ์ของการใช้กฎการพิสูจน์กับประโยคก่อนหน้าในลำดับ^{[ 19 ]}แต่ละบรรทัดของการพิสูจน์ประกอบด้วยประโยคการพิสูจน์พร้อมด้วยคำอธิบายประกอบชุดข้อสมมติและหมายเลขบรรทัดปัจจุบัน^{[ 19 ]}ชุดข้อสมมติแสดงรายการข้อสมมติที่ประโยคการพิสูจน์ที่กำหนดขึ้นนั้นขึ้นอยู่กับ ซึ่งอ้างอิงโดยหมายเลขบรรทัด^{[ 19 ]}คำอธิบายประกอบระบุว่าใช้กฎการพิสูจน์ใด และกับบรรทัดก่อนหน้าใด เพื่อให้ได้ประโยคปัจจุบัน^{[ 19 ]}นี่คือตัวอย่างการพิสูจน์:

การพิสูจน์แบบ Suppes–Lemmon (ตัวอย่างแรก)

${\displaystyle P\to Q,\neg Q\vdash \neg P}$
ชุดสมมติฐาน	หมายเลขบรรทัด	สูตร ( wff )	คำอธิบายประกอบ
1	1	${\displaystyle P\to Q}$	เอ
2	2	${\displaystyle \neg Q}$	เอ
3	3	${\displaystyle P}$	เอ
1, 3	4	${\displaystyle Q}$	1, 3 →E
1, 2	5	${\displaystyle \neg P}$	2, 4 RAA
QED

การพิสูจน์นี้จะชัดเจนยิ่งขึ้นเมื่อมีการระบุหลักเกณฑ์การอนุมานและคำอธิบายประกอบที่เหมาะสม – ดูหัวข้อ§ หลักเกณฑ์การอนุมานเชิงประพจน์ (แบบ Suppes–Lemmon )

ส่วนนี้จะกำหนดไวยากรณ์เชิงรูปธรรมสำหรับภาษาตรรกศาสตร์เชิงประพจน์โดยเปรียบเทียบวิธีการทั่วไปในการกำหนดไวยากรณ์ดังกล่าวกับวิธีการแบบเกนท์เซน (Gentzen-style)

ในแคลคูลัสเชิงประพจน์แบบคลาสสิก ภาษาเชิงรูปธรรมมักจะถูกกำหนด (ในที่นี้: โดยการเรียกซ้ำ ) ดังนี้: ^{[ 20 ]}${\displaystyle {\mathcal {L}}}$

1. ตัวแปรเชิงประพจน์แต่ละตัวเป็นสูตร
2. " " คือสูตร${\displaystyle \bot }$
3. ถ้าและเป็นสูตร ดังนั้น, , , ก็เป็นสูตรเช่น กัน${\displaystyle \varphi }$${\displaystyle \psi }$${\displaystyle (\varphi \land \psi )}$${\displaystyle (\varphi \lor \psi )}$${\displaystyle (\varphi \to \psi )}$${\displaystyle (\varphi \leftrightarrow \psi )}$
4. ไม่มีอะไรอื่นที่เป็นสูตรสำเร็จอีกแล้ว

การปฏิเสธ ( ) ถูกนิยามว่าเป็นการบ่งชี้ถึงความเท็จ${\displaystyle \neg }$

${\displaystyle \neg \phi \;{\overset {\text{def}}{=}}\;\phi \to \bot }$,

โดยที่(falsum) หมายถึงความขัดแย้งหรือความเท็จโดยสิ้นเชิง^{[ 21 ] [ 22 ] [ 23 ] [ 24 ] [ 25 ]}${\displaystyle \bot }$

สิ่งพิมพ์เก่าๆ และสิ่งพิมพ์ที่ไม่ได้เน้นระบบตรรกะ เช่น ระบบขั้นต่ำ ระบบ เชิงสัญชาตญาณหรือระบบฮิลเบิร์ตถือว่าการปฏิเสธเป็นตัวเชื่อมตรรกะ พื้นฐาน ซึ่งหมายความว่าถือว่าเป็นการดำเนินการพื้นฐานและไม่ได้กำหนดในแง่ของตัวเชื่อมอื่นๆ^{[ 26 ] [ 27 ]}ผู้เขียนบางคน เช่นBostockใช้และและยังกำหนดให้เป็นตัวเชื่อมพื้นฐาน อีกด้วย ^{[ 28 ] [ 29 ]}${\displaystyle \bot }$${\displaystyle \top }$${\displaystyle \neg }$

คำจำกัดความของไวยากรณ์ยังสามารถกำหนดได้โดยใช้สัญกรณ์ต้นไม้ของ Gentzenโดยการเขียนสูตรที่ถูกต้องไว้ด้านล่างเส้นอนุมานและตัวแปรแผนผังใดๆ ที่ใช้โดยสูตรเหล่านั้นไว้ด้านบน^{[ 26 ]}ตัวอย่างเช่น สิ่งที่เทียบเท่ากับกฎข้อ 3 และ 4 จากคำจำกัดความของ Bostock ข้างต้น เขียนได้ดังนี้:

${\displaystyle {\frac {\varphi }{(\neg \varphi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \lor \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \land \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \rightarrow \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \leftrightarrow \psi )}}}$.

ข้อตกลงการเขียนสัญลักษณ์ที่แตกต่างกันมองว่าไวยากรณ์ของภาษาเป็นไวยากรณ์เชิงหมวดหมู่ที่มีหมวดหมู่เดียวคือ "สูตร" ซึ่งแสดงด้วยสัญลักษณ์ดังนั้นองค์ประกอบใด ๆ ของไวยากรณ์จึงถูกนำเสนอโดยการจัดหมวดหมู่ ซึ่งใช้สัญลักษณ์หมายความว่า " เป็นนิพจน์สำหรับวัตถุในหมวดหมู่" ^{[ 30 ]}จากนั้นตัวอักษรประโยคจะถูกนำเสนอโดยการจัดหมวดหมู่ เช่น, , , และอื่นๆ^{[ 30 ]}ในทางกลับกัน ตัวเชื่อมจะถูกกำหนดโดยข้อความที่คล้ายกับข้างต้น แต่ใช้สัญลักษณ์การจัดหมวดหมู่ ดังที่เห็นด้านล่าง: ${\displaystyle {\mathcal {F}}}$${\displaystyle \varphi :{\mathcal {F}}}$${\displaystyle \varphi }$${\displaystyle {\mathcal {F}}}$${\displaystyle P:{\mathcal {F}}}$${\displaystyle Q:{\mathcal {F}}}$${\displaystyle R:{\mathcal {F}}}$

ตัวเชื่อมที่กำหนดผ่านไวยากรณ์เชิงหมวดหมู่^{[ 30 ]}

คำสันธาน (&)	การแยก (∨)	นัยยะ (→)	การปฏิเสธ (¬)
${\displaystyle {\frac {A:{\mathcal {F}}\quad B:{\mathcal {F}}}{\&(A)(B):{\mathcal {F}}}}}$	${\displaystyle {\frac {A:{\mathcal {F}}\quad B:{\mathcal {F}}}{\vee (A)(B):{\mathcal {F}}}}}$	${\displaystyle {\frac {A:{\mathcal {F}}\quad B:{\mathcal {F}}}{{\mathord {\supset }}(A)(B):{\mathcal {F}}}}}$	${\displaystyle {\frac {A:{\mathcal {F}}}{\neg (A):{\mathcal {F}}}}}$

ในส่วนที่เหลือของบทความนี้จะใช้สัญลักษณ์การจัดหมวดหมู่สำหรับข้อความใดๆ ที่ใช้สัญลักษณ์เกนท์เซน (Gentzen-notation) เพื่ออธิบายไวยากรณ์ของภาษา ส่วนข้อความอื่นๆ ที่ใช้สัญลักษณ์เกนท์เซนจะเป็นการอนุมาน โดยยืนยันว่าลำดับ (sequent) เป็นไปตามนั้น ไม่ใช่ยืนยันว่านิพจน์นั้นเป็นสูตรที่ถูกต้อง ${\displaystyle \varphi :{\mathcal {F}}}$

ให้ภาษาประพจน์ถูกกำหนดแบบอุปนัยดังนี้ ${\displaystyle {\mathcal {L}}}$${\displaystyle \Phi ::=p_{1},p_{2},\dots \mid \bot \mid (\Phi \to \Phi )\mid (\Phi \land \Phi )\mid (\Phi \lor \Phi )}$

นิยามการปฏิเสธว่าคือ. ${\displaystyle \neg \Phi \,{\overset {\text{def}}{=}}\,(\Phi \to \bot )}$

ต่อไปนี้เป็นรายการของกฎการอนุมานเบื้องต้นสำหรับการหักล้างตามธรรมชาติในตรรกะเชิงประพจน์: ^{[ 31 ] [ 26 ]}

กฎสำหรับตรรกศาสตร์เชิงประพจน์

กฎการแนะนำ	กฎการคัดออก
${\displaystyle {\begin{array}{c}\varphi \qquad \psi \\\hline \varphi \land \psi \end{array}}(\land _{I})}$	${\displaystyle {\begin{array}{c}\varphi \land \psi \\\hline \varphi \end{array}}(\land _{E})}$
${\displaystyle {\begin{array}{c}\varphi \\\hline \varphi \lor \psi \end{array}}(\lor _{I})}$	${\displaystyle {\cfrac {\varphi \lor \psi \quad {\begin{matrix}[\varphi ]^{u}\\\vdots \\\chi \end{matrix}}\quad {\begin{matrix}[\psi ]^{v}\\\vdots \\\chi \end{matrix}}}{\chi }}\ \lor _{E^{u,v}}}$
${\displaystyle {\begin{array}{c}[\varphi ]^{u}\\\vdots \\\psi \\\hline \varphi \to \psi \end{array}}(\to _{I})\ u}$	${\displaystyle {\begin{array}{c}\varphi \qquad \varphi \to \psi \\\hline \psi \end{array}}(\to _{E})}$
	${\displaystyle {\begin{array}{c}\bot \\\hline \varphi \end{array}}(\bot _{E})}$
	[ 32 ]${\displaystyle {\begin{array}{c}(\varphi \to \bot )\to \bot \\\hline \varphi \end{array}}(\neg \neg _{E})}$

ในตารางนี้ ตัวอักษรกรีกคือแผนผังซึ่งครอบคลุมสูตรต่างๆ มากกว่าที่จะครอบคลุมเฉพาะประพจน์พื้นฐานเท่านั้น ชื่อของกฎจะอยู่ทางด้านขวาของแผนผังสูตร ตัวอย่างเช่น กฎการแนะนำข้อแรกมีชื่อว่าซึ่งย่อมาจาก "การแนะนำคำสันธาน" ${\displaystyle \varphi ,\psi ,\chi }$${\displaystyle \land _{I}}$

• ตรรกะขั้นต่ำ : กฎการอนุมานตามธรรมชาติคือ...${\displaystyle ND_{MPC}=\{\land _{I},\land _{E},\lor _{I},\lor _{E},\to _{I},\to _{E}\}}$

หากไม่มีกฎเกณฑ์และระบบจะกำหนดตรรกะขั้นต่ำ (ตามที่Johansson ได้กล่าวไว้ ) ^{[ 33 ]}${\displaystyle \bot _{E}}$${\displaystyle \neg \neg _{E}}$

• ตรรกศาสตร์เชิงสัญชาตญาณ : กฎการอนุมานตามธรรมชาติคือ...${\displaystyle ND_{IPC}=ND_{MPC}\cup \{\bot _{E}\}}$

เมื่อเพิ่มกฎ( หลักการระเบิด ) เข้าไปในกฎของตรรกะขั้นต่ำ ระบบจะกำหนดตรรกะแบบสัญชาตญาณขึ้นมา${\displaystyle \bot _{E}}$

ข้อความดังกล่าวถูกต้อง (แม้ในตรรกะขั้นต่ำ ดูตัวอย่างที่ 1 ด้านล่าง) ซึ่งแตกต่างจากการอนุมานแบบย้อนกลับซึ่งจะนำไปสู่กฎของสิ่งที่ไม่รวมอยู่ตรงกลาง${\displaystyle P\to \neg \neg P}$

• ตรรกศาสตร์คลาสสิก : กฎการอนุมานตามธรรมชาติคือ ^{[ 32 ]}${\displaystyle ND_{CPC}=ND_{IPC}\cup \{\neg \neg _{E}\}}$

เมื่อกฎการอนุมานตามธรรมชาติที่ระบุไว้ทั้งหมดได้รับการยอมรับ ระบบจะกำหนดตรรกะแบบคลาสสิก^{[ 34 ] [ 35 ] [ 36 ]}

ตัวอย่างที่ 1 : ^{[ 24 ]}พิสูจน์ภายในตรรกะขั้นต่ำของ. ${\displaystyle P\to \neg \neg P}$

เป้าหมาย: พิสูจน์: ${\displaystyle P\to ((P\to \bot )\to \bot )}$

${\displaystyle {\cfrac {{\cfrac {[P]^{v}\qquad [P\to \bot ]^{u}}{\bot }}\to _{E}}{{\cfrac {((P\to \bot )\to \bot )}{P\to ((P\to \bot )\to \bot )}}\to _{I^{v}}}}\to _{I^{u}}}$

ตัวอย่างที่ 2 : การพิสูจน์โดยใช้ตรรกะขั้นต่ำของ: ${\displaystyle A\to \left(B\to \left(A\land B\right)\right)}$

${\displaystyle {\cfrac {{\cfrac {[A]^{u}\quad [B]^{w}}{A\land B}}\ \land _{I}}{{\cfrac {B\to \left(A\land B\right)}{A\to \left(B\to \left(A\land B\right)\right)}}\ \to _{I^{u}}}}\ \to _{I^{w}}}$

ฟิตช์ได้พัฒนาระบบการอนุมานเชิงธรรมชาติซึ่งมีลักษณะดังนี้

• การนำเสนอการพิสูจน์แบบเชิงเส้น แทนที่จะนำเสนอในรูปแบบแผนผังต้นไม้
• การพิสูจน์ย่อยซึ่งสามารถเปิดข้อสมมติภายในการพิสูจน์ย่อยและยกเลิกข้อสมมติเหล่านั้นในภายหลังได้

ต่อมานักตรรกศาสตร์และนักการศึกษา เช่นPatrick Suppes ^{[ 37 ]}และEJ Lemmon ^{[ 38 ]}ได้เปลี่ยนชื่อระบบของ Fitch ใหม่ แม้ว่าพวกเขาจะนำการเปลี่ยนแปลงทางกราฟิกมาใช้ เช่น การแทนที่การเยื้องด้วยเส้นแนวตั้ง แต่โครงสร้างพื้นฐานของการอนุมานตามธรรมชาติแบบ Fitch ยังคงอยู่เหมือนเดิม รูปแบบต่างๆ เหล่านี้มักถูกเรียกว่ารูปแบบ Suppes–Lemmon แม้ว่าโดยพื้นฐานแล้วจะอิงตามสัญกรณ์ดั้งเดิมของ Fitch ก็ตาม

การนำเสนอแบบเชิงเส้นที่ใช้ในบทพิสูจน์แบบ Fitch และ Suppes–Lemmon — โดยใช้หมายเลขบรรทัดและการจัดแนวแนวตั้ง/ชุดสมมติฐาน — ทำให้บทพิสูจน์ย่อยมองเห็นได้ชัดเจน Fitch (อย่างประหยัดและระมัดระวัง) ใช้กฎที่ได้มา Suppes–Lemmon ไปไกลกว่านั้นและเพิ่มกฎที่ได้มาเข้าไปในชุดเครื่องมือของกฎการอนุมานตามธรรมชาติ

Suppes ได้นำเสนอการอนุมานตามธรรมชาติโดยใช้กฎแบบ Gentzen ^{[ 37 ]}

• เขาให้นิยามการปฏิเสธในแง่ของความขัดแย้ง:${\displaystyle \neg P\equiv (P\to \bot )}$
• เขาอธิบายกฎที่ได้มาอย่างชัดเจน แม้ว่าจะไม่ได้แยกแยะความแตกต่างระหว่างกฎเหล่านั้นกับกฎพื้นฐานอย่างชัดเจนเสมอไปในแง่ของโครงสร้างก็ตาม
• ระบบของเขานั้นเรียบง่ายมาก แต่ก็ยังมีขั้นตอนย่อยเพื่อความกระชับ

เลมมอนได้กำหนดกฎเกณฑ์ที่ได้มาอย่างเป็นทางการมากขึ้น^{[ 38 ]}เขายังกำหนดนิยามของการปฏิเสธเป็นการบ่งชี้ถึงความเท็จด้วย: นี่ไม่ได้ระบุไว้เป็นนิยามอย่างเป็นทางการในตรรกศาสตร์เบื้องต้นแต่ถือว่ามีนัยยะแฝงอยู่ตลอดทั้งระบบ นี่คือวิธีที่เราทราบ: ${\displaystyle \neg P\equiv P\to \bot }$

• การใช้ RAA (Reductio ad Absurdum): เลมมอนใช้ RAA เป็นประจำในรูปแบบ: สมมติพิสูจน์แล้วจึงสรุป${\displaystyle P}$${\displaystyle \bot }$${\displaystyle \neg P}$

วิธีนี้ใช้ได้ผลก็ต่อเมื่อเข้าใจว่าเป็น.${\displaystyle \neg P}$${\displaystyle P\to \bot }$

• การพิสูจน์โดยใช้ความขัดแย้ง: เลมมอนใช้ข้อเท็จจริงที่ว่าจากสิ่งหนึ่งสามารถอนุมานได้อีกสิ่งหนึ่งได้${\displaystyle \neg P\land P}$${\displaystyle \bot }$

วิธีนี้จำเป็นต้องปฏิบัติต่อสิ่งนั้นในลักษณะที่ว่า modus ponens จะนำไปสู่ความขัดแย้ง${\displaystyle \neg P}$${\displaystyle P\to \bot }$

• การไม่มีกฎพื้นฐานสำหรับ “¬”: เลมมอนไม่ได้รวมกฎเฉพาะสำหรับการนำ “¬” มาใช้หรือกำจัดออกไป แต่เขาได้อนุมานการปฏิเสธโดยใช้การบ่งชี้และการขัดแย้งแทน

ในตารางด้านล่าง อ้างอิงจาก Lemmon (1978) ^{[ 39 ]}และ Allen & Hand (2022) ^{[ 19 ]}กฎที่ Lemmon ได้มาจะถูกเน้นไว้ กฎ เหล่านี้สามารถอนุมานได้จากกฎของ Gentzen (ที่ไม่ได้เน้น)

มีกฎการพิสูจน์พื้นฐานเก้าข้อ ได้แก่ กฎการสมมติบวกกับกฎการแนะนำและการกำจัดสี่คู่สำหรับตัวเชื่อมไบนารี และกฎการปฏิเสธซ้ำซ้อนและการหักล้างแบบไร้สาระซึ่งจำเป็นต้องใช้เพียงข้อเดียว^{[ 32 ] [ 19 ]}ตรรกบทแบบแยกส่วนสามารถใช้เป็นทางเลือกที่ง่ายกว่าการกำจัด ∨ ที่เหมาะสม^{[ 19 ]}และ MTT เป็นกฎที่กำหนดโดยทั่วไป^{[ 39 ]}แม้ว่าจะไม่ใช่กฎพื้นฐานก็ตาม^{[ 19 ]}

รายการกฎการอนุมาน

ชื่อกฎ	ชื่อเรียกอื่น	คำอธิบายประกอบ	ชุดสมมติฐาน	คำแถลง
กฎแห่งสมมติฐาน	สมมติฐาน	เอ	หมายเลขสายปัจจุบัน	ในทุกขั้นตอนของการโต้แย้ง ให้เสนอข้อเสนอแนะในฐานะข้อสันนิษฐานของการโต้แย้งนั้น
บทนำของคำสันธาน	การแนะนำแอมเปอร์แซนด์ การเชื่อมโยง (CONJ) [ 40 ]	ม, น และ ไอ	การรวมกันของชุดสมมติฐานที่เส้น mและn	จากเส้นmและnให้สรุปได้ว่า ${\displaystyle \varphi }$${\displaystyle \psi }$${\displaystyle \varphi \land \psi }$
การกำจัดคำสันธาน	การทำให้ง่ายขึ้น (S) การกำจัดเครื่องหมายแอมเปอร์แซนด์	ฉัน	เช่นเดียวกับที่บรรทัด m	จากบรรทัดmให้ อนุมานและ${\displaystyle \varphi \land \psi }$${\displaystyle \varphi }$${\displaystyle \psi }$
บทนำการแยก	การบวก (ADD)	ม ∨I	เช่นเดียวกับที่บรรทัด m	จากบรรทัดที่mให้อนุมานว่าอะไรก็ตาม ${\displaystyle \varphi }$${\displaystyle \varphi \lor \psi }$${\displaystyle \psi }$
การกำจัดการแยก	การกำจัดลิ่ม, ภาวะกลืนไม่เข้าคายไม่ออก (DL) [ 40 ]	j,k,l,m,n ∨E	เส้นj,k,l,m, n	จากบรรทัดjและสมมติฐานของบรรทัดkและการอนุมานของจากบรรทัดlและสมมติฐานของบรรทัดmและการอนุมานของจากบรรทัดnสรุปได้ว่า ${\displaystyle \varphi \lor \psi }$${\displaystyle \varphi }$${\displaystyle \chi }$${\displaystyle \varphi }$${\displaystyle \psi }$${\displaystyle \chi }$${\displaystyle \psi }$${\displaystyle \chi }$
บทนำของลูกศร	การพิสูจน์แบบมีเงื่อนไข (CP) [ 40 ]การแนะนำแบบมีเงื่อนไข	n, →I (m)	ทุกอย่างในชุดสมมติฐานที่บรรทัดnยกเว้นmซึ่งเป็นบรรทัดที่ถือว่าเงื่อนไขก่อนหน้าเป็นจริง	จากบรรทัดที่nโดยอ้างอิงจากสมมติฐานของบรรทัดที่mให้สรุปได้ว่า ${\displaystyle \psi }$${\displaystyle \varphi }$${\displaystyle \varphi \to \psi }$
การกำจัดลูกศร	Modus ponendo ponens (MPP), modus ponens (MP), [ 40 ]การกำจัดแบบมีเงื่อนไข	ม, น →E	การรวมกันของชุดสมมติฐานที่เส้น mและn	จากบรรทัดmและบรรทัดnให้สรุปได้ว่า ${\displaystyle \varphi \to \psi }$${\displaystyle \varphi }$${\displaystyle \psi }$
การปฏิเสธซ้ำซ้อน[ 40 ]	การกำจัดการปฏิเสธซ้ำซ้อน	ม. ดีเอ็น	เช่นเดียวกับที่บรรทัด m	จากบรรทัดที่mให้สรุปได้ว่า... ${\displaystyle \neg \neg \varphi }$${\displaystyle \varphi }$
Reductio ad absurdum	การพิสูจน์ทางอ้อม (IP), การแนะนำการปฏิเสธ (¬I), การกำจัดการปฏิเสธ (¬E)	ม,  น RAA  (k)	การรวมกันของชุดสมมติฐานที่บรรทัดmและnโดยไม่รวมk (สมมติฐานที่ถูกปฏิเสธ)	เพื่อลดความซับซ้อนของข้อความของกฎ คำว่า "การปฏิเสธ" ในที่นี้ใช้ในลักษณะนี้: การปฏิเสธสูตรที่ไม่ใช่การปฏิเสธคือในขณะที่การปฏิเสธมีการปฏิเสธ สองแบบ คือและที่บรรทัดmและnอนุมานการปฏิเสธสมมติฐานใดๆ ที่ปรากฏในบทพิสูจน์ (ที่บรรทัดk ) ${\displaystyle \varphi }$${\displaystyle \neg \varphi }$${\displaystyle \neg \varphi }$${\displaystyle \varphi }$${\displaystyle \neg \neg \varphi }$
ตรรกบทแบบแยกส่วน	การกำจัดลิ่ม (∨E), โหมดโทลเลนโดโพเนน (MTP)	ม,น DS	การรวมกันของชุดสมมติฐานที่เส้น mและn	จากบรรทัดmและบรรทัดnให้สรุปได้ว่าจากบรรทัดmและบรรทัดnให้สรุปได้ว่า ${\displaystyle \varphi \lor \psi }$${\displaystyle \neg \varphi }$${\displaystyle \psi }$${\displaystyle \varphi \lor \psi }$${\displaystyle \neg \psi }$${\displaystyle \varphi }$
การแนะนำลูกศรคู่	นิยามแบบสองเงื่อนไข ( Df ), การแนะนำแบบสองเงื่อนไข ${\displaystyle \leftrightarrow }$	ม, นฉัน${\displaystyle \leftrightarrow }$	การรวมกันของชุดสมมติฐานที่เส้น mและn	จากเส้นmและnให้สรุปได้ว่า ${\displaystyle \varphi \to \psi }$${\displaystyle \psi \to \varphi }$${\displaystyle \varphi \leftrightarrow \psi }$
การกำจัดด้วยลูกศรคู่	นิยามแบบสองเงื่อนไข ( Df ) การกำจัดแบบสองเงื่อนไข ${\displaystyle \leftrightarrow }$	ฉัน​${\displaystyle \leftrightarrow }$	เช่นเดียวกับที่บรรทัด m	จากบรรทัดที่mให้สรุปได้ว่า เป็นอย่างใดอย่างหนึ่ง ${\displaystyle \varphi \leftrightarrow \psi }$${\displaystyle \varphi \to \psi }$${\displaystyle \psi \to \varphi }$
Modus tollendo tollens	โมดัส โทลเลนส์ (MT)	ม., น. เอ็มทีที	การรวมกันของชุดสมมติฐานที่เส้น mและn	จากบรรทัดmและบรรทัดnให้สรุปได้ว่า ${\displaystyle \varphi \to \psi }$${\displaystyle \neg \psi }$${\displaystyle \neg \varphi }$

โปรดจำไว้ว่าตัวอย่างการพิสูจน์ได้แสดงไว้แล้วเมื่อแนะนำสัญกรณ์ § Suppes–Lemmonนี่คือตัวอย่างที่สอง

การพิสูจน์แบบ Suppes–Lemmon (ตัวอย่างที่สอง)

${\displaystyle P\lor Q,\neg P,\neg P\to \neg Q\vdash \bot }$ความขัดแย้ง
ชุดสมมติฐาน	หมายเลขบรรทัด	สูตร	คำอธิบายประกอบ
1	1	${\displaystyle P\lor Q}$	เอ
2	2	${\displaystyle \neg P}$	เอ
3	3	${\displaystyle \neg P\to \neg Q}$	เอ
2,3	4	${\displaystyle \neg Q}$	2, 3 →E
1,2,3	5	${\displaystyle P}$	ก (หลักฐานย่อย)
1,2,3,5	6	${\displaystyle \bot }$	2, 5 RAA [ 41 ]
1,2,3	7	${\displaystyle Q}$	ก (หลักฐานย่อย)
1,2,3,7	8	${\displaystyle \bot }$	4, 7 RAA [ 41 ]
1,2,3	9	${\displaystyle \bot }$	1, 5–6, 7–8 vE
QED

การพิสูจน์ต่อไปนี้แสดงให้เห็นถึงสองทฤษฎีบท:

• บรรทัดที่ 1-8 พิสูจน์โดยใช้ตรรกะขั้นต่ำ :

${\displaystyle \vdash _{MPC}\neg \neg (P\lor \neg P)}$.

• บรรทัดที่ 1-9 พิสูจน์ได้ด้วยตรรกศาสตร์แบบคลาสสิก :

${\displaystyle \vdash _{CPC}P\lor \neg P}$.

เป้าหมาย:

• บรรทัดที่ 1 - 8: .${\displaystyle \vdash _{MPC}((P\lor (P\to \bot ))\to \bot )\to \bot }$
• บรรทัดที่ 1 - 9: .${\displaystyle \vdash _{CPC}P\lor (P\to \bot )}$

การพิสูจน์แบบ Suppes–Lemmon (ตัวอย่างที่สาม)

${\displaystyle \vdash P\lor \neg P}$
ชุดสมมติฐาน	หมายเลขบรรทัด	สูตร	คำอธิบายประกอบ
1	1	${\displaystyle (P\lor (P\to \bot ))\to \bot }$	เอ
1, 2	2	${\displaystyle P}$	เอ
1, 2	3	${\displaystyle P\lor (P\to \bot )}$	2, ∨I
1, 2	4	${\displaystyle \bot }$	1, 3, →E
1	5	${\displaystyle P\to \bot }$	2, 4, →I (คายประจุ 2)
1	6	${\displaystyle P\lor (P\to \bot )}$	5, ∨I
1	7	${\displaystyle \bot }$	1, 6, →E
∅	8	${\displaystyle ((P\lor (P\to \bot ))\to \bot )\to \bot }$	1, 7, →I (คายประจุ 1)
∅	9	${\displaystyle P\lor (P\to \bot )}$	8, DN
QED

หมายเหตุ : วาเลรี กลิเวนโกได้พิสูจน์ทฤษฎีบทต่อไปนี้:

ถ้าเป็นสูตรเชิงประพจน์แล้วจะเป็นสัจนิรันดร์ แบบคลาสสิก ก็ต่อเมื่อเป็นสัจนิรันดร์แบบสัญชาตญาณนิยม${\displaystyle \varphi }$${\displaystyle \varphi }$${\displaystyle \neg \neg \varphi }$

นี่หมายความว่าทฤษฎีบทเชิงประพจน์แบบคลาสสิกทั้งหมดสามารถพิสูจน์ได้ดังตัวอย่างนี้: ${\displaystyle \varphi }$

1. พิสูจน์โดยใช้ตรรกะแบบสัญชาตญาณ (กล่าวคือ โดยไม่ต้องใช้)${\displaystyle \neg \neg \varphi }$${\displaystyle \neg \neg _{E}}$
2. สมัครเพื่อรับจาก.${\displaystyle \neg \neg _{E}}$${\displaystyle \varphi }$${\displaystyle \neg \neg \varphi }$

กล่าวได้ว่าทฤษฎีมีความสอดคล้องหากไม่สามารถพิสูจน์ความเท็จได้ (โดยไม่ต้องมีข้อสมมติใดๆ) และสมบูรณ์หากสามารถพิสูจน์ทฤษฎีบทหรือข้อปฏิเสธของทฤษฎีบททุกข้อได้โดยใช้กฎการอนุมานของตรรกศาสตร์ สิ่งเหล่านี้เป็นข้อความเกี่ยวกับตรรกศาสตร์ทั้งหมด และมักจะเชื่อมโยงกับแนวคิดของแบบจำลองบางอย่างอย่างไรก็ตามมีแนวคิดเรื่องความสอดคล้องและความสมบูรณ์ในระดับท้องถิ่นที่เป็นเพียงการตรวจสอบทางไวยากรณ์ของกฎการอนุมาน และไม่จำเป็นต้องอ้างอิงถึงแบบจำลอง ประการแรกคือ ความสอดคล้องในระดับท้องถิ่น หรือที่เรียกว่า ความสามารถในการลดทอนในระดับท้องถิ่น ซึ่งกล่าวว่า การอนุมานใดๆ ที่มีการแนะนำตัวเชื่อมตามด้วยการกำจัดตัวเชื่อมนั้นทันที สามารถเปลี่ยนเป็น1การอนุมานที่เทียบเท่ากันได้โดยไม่ต้องอ้อม นี่เป็นการตรวจสอบความแข็งแกร่งของกฎการกำจัด: กฎเหล่านั้นต้องไม่แข็งแกร่งเกินไปจนรวมถึงความรู้ที่ไม่ได้อยู่ในข้อตั้งต้นอยู่แล้ว ตัวอย่างเช่น พิจารณาคำสันธานเชื่อมประโยค

${\displaystyle {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\ }}u\qquad {\cfrac {}{B\ }}w}{A\wedge B\ }}\wedge _{I}}{A\ }}\wedge _{E1}\end{aligned}}\quad \Rightarrow \quad {\cfrac {}{A\ }}u}$

ในทำนองเดียวกัน ความสมบูรณ์ในระดับท้องถิ่นกล่าวว่ากฎการกำจัดนั้นแข็งแกร่งพอที่จะแยกคำเชื่อมออกเป็นรูปแบบที่เหมาะสมกับกฎการแนะนำของมัน เช่นเดียวกับคำสันธาน:

${\displaystyle {\cfrac {}{A\wedge B\ }}u\quad \Rightarrow \quad {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\wedge B\ }}u}{A\ }}\wedge _{E1}\qquad {\cfrac {{\cfrac {}{A\wedge B\ }}u}{B\ }}\wedge _{E2}}{A\wedge B\ }}\wedge _{I}\end{aligned}}}$

แนวคิดเหล่านี้สอดคล้องกับการลด β (beta reduction)และการแปลง η (eta conversion)ในแคลคูลัสแลมบ์ดา อย่างแม่นยำ โดยใช้ไอโซมอร์ฟิซึม Curry–Howardโดยความสมบูรณ์ในระดับท้องถิ่น เราจะเห็นว่าการอนุมานทุกแบบสามารถแปลงเป็นการอนุมานที่เทียบเท่ากันได้ โดยที่ตัวเชื่อมหลักจะถูกแนะนำเข้ามา ในความเป็นจริง หากการอนุมานทั้งหมดปฏิบัติตามลำดับการกำจัดตามด้วยการแนะนำนี้ ก็จะกล่าวได้ว่าเป็นการ อนุมาน ปกติในการอนุมานปกติ การกำจัดทั้งหมดจะเกิดขึ้นเหนือการแนะนำ ในตรรกะส่วนใหญ่ การอนุมานทุกแบบมีการอนุมานปกติที่เทียบเท่ากัน เรียกว่ารูปแบบปกติการมีอยู่ของรูปแบบปกติโดยทั่วไปยากที่จะพิสูจน์ได้โดยใช้การอนุมานตามธรรมชาติเพียงอย่างเดียว แม้ว่าจะมีคำอธิบายดังกล่าวอยู่ในวรรณกรรม โดยเฉพาะอย่างยิ่งโดยDag Prawitzในปี 1961 ^{[ 42 ]}การแสดงสิ่งนี้โดยอ้อมโดยใช้การนำเสนอ แคลคูลัสลำดับแบบไม่มีการตัดนั้น ง่ายกว่ามาก

ตรรกะในส่วนก่อนหน้านี้เป็นตัวอย่างของตรรกะแบบประเภทเดียว กล่าวคือตรรกะที่มีวัตถุเพียงชนิดเดียว: ประพจน์ มีการเสนอส่วนขยายมากมายของกรอบงานที่เรียบง่ายนี้ ในส่วนนี้เราจะขยายมันด้วยบุคคลหรือเทอม ประเภทที่สอง กล่าวคือ เราจะเพิ่มหมวดหมู่ใหม่ "เทอม" ซึ่งใช้สัญลักษณ์เราจะกำหนดเซตของตัวแปรที่นับได้เซตของสัญลักษณ์ฟังก์ชัน ที่นับได้อีกเซตหนึ่ง และสร้างเทอมด้วยกฎการสร้างต่อไปนี้: ${\displaystyle {\mathcal {T}}}$${\displaystyle V}$${\displaystyle F}$

${\displaystyle {\frac {v\in V}{v:{\mathcal {T}}}}{\hbox{ var}}_{F}}$

และ

${\displaystyle {\frac {f\in F\qquad t_{1}:{\mathcal {T}}\qquad t_{2}:{\mathcal {T}}\qquad \cdots \qquad t_{n}:{\mathcal {T}}}{f(t_{1},t_{2},\cdots ,t_{n}):{\mathcal {T}}}}{\hbox{ app}}_{F}}$

สำหรับข้อเสนอ เราพิจารณาเซตย่อยที่นับได้ชุดที่สามPของภาคแสดงและกำหนดภาคแสดงอะตอมิกเหนือเทอมด้วยกฎการสร้างต่อไปนี้:

${\displaystyle {\frac {\phi \in P\qquad t_{1}:{\mathcal {T}}\qquad t_{2}:{\mathcal {T}}\qquad \cdots \qquad t_{n}:{\mathcal {T}}}{\phi (t_{1},t_{2},\cdots ,t_{n}):{\mathcal {F}}}}{\hbox{ pred}}_{F}}$

กฎการสร้างสองข้อแรกให้คำจำกัดความของคำศัพท์ที่เหมือนกับคำจำกัดความในพีชคณิตคำศัพท์และทฤษฎีแบบจำลอง แม้ว่าจุดเน้นของสาขาวิชาเหล่านั้นจะแตกต่างจากการอนุมานตามธรรมชาติก็ตาม กฎการสร้างข้อที่สามให้คำจำกัดความของ สูตรอะตอมอย่างมีประสิทธิภาพเช่นเดียวกับในตรรกศาสตร์ลำดับที่หนึ่งและอีกครั้งในทฤษฎีแบบจำลอง

นอกจากนี้ ยังมีการเพิ่มกฎการสร้างประโยคอีกสองข้อ ซึ่งกำหนดสัญลักษณ์สำหรับ ประโยค ที่มีตัวบ่งปริมาณข้อหนึ่งสำหรับตัวบ่งปริมาณสากล (∀) และตัวบ่งปริมาณเชิงมีอยู่ (∃):

${\displaystyle {\frac {x\in V\qquad A:{\mathcal {F}}}{\forall x.A:{\mathcal {F}}}}\;\forall _{F}\qquad \qquad {\frac {x\in V\qquad A:{\mathcal {F}}}{\exists x.A:{\mathcal {F}}}}\;\exists _{F}}$

ตัวบ่งปริมาณสากลมีกฎการนำมาใช้และการละเว้น:

${\displaystyle {\cfrac {\begin{array}{c}{\cfrac {}{a:{\mathcal {T}}}}{\text{ u}}\\\vdots \\{}[a/x]A\end{array}}{\forall x.A}}\;\forall _{I^{u,a}}\qquad \qquad {\frac {\forall x.A\qquad t:{\mathcal {T}}}{[t/x]A}}\;\forall _{E}}$

ตัวบ่งปริมาณเชิงการมีอยู่มีกฎการนำเข้าและการกำจัด:

${\displaystyle {\frac {[t/x]A}{\exists x.A}}\;\exists _{I}\qquad \qquad {\cfrac {\begin{array}{cc}&\underbrace {\,{\cfrac {}{a:{\mathcal {T}}}}{\hbox{ u}}\quad {\cfrac {}{[a/x]A}}{\hbox{ v}}\,} \\&\vdots \\\exists x.A\quad &C\\\end{array}}{C}}\exists _{E^{a,u,v}}}$

ในกฎเหล่านี้ สัญลักษณ์ [ t / x ] Aหมายถึงการแทนที่tสำหรับทุกอินสแตนซ์ (ที่มองเห็นได้) ของxในAโดยหลีกเลี่ยงการจับ^{[ 43 ]}เช่นเดียวกับก่อนหน้านี้ ตัวยกบนชื่อหมายถึงส่วนประกอบที่ถูกปลดออก: เทอมaไม่สามารถปรากฏในข้อสรุปของ ∀I (เทอมดังกล่าวเรียกว่าตัวแปรลักษณะเฉพาะหรือพารามิเตอร์ ) และสมมติฐานที่ชื่อuและvใน ∃E จะถูกจำกัดไว้ที่ข้อตั้งต้นที่สองในการอนุมานเชิงสมมติฐาน แม้ว่าตรรกะเชิงประพจน์ของส่วนก่อนหน้านี้จะสามารถตัดสินได้การเพิ่มตัวบ่งปริมาณทำให้ตรรกะไม่สามารถตัดสินได้

จนถึงตอนนี้ ส่วนขยายเชิงปริมาณเป็นลำดับที่หนึ่ง กล่าวคือ พวกมันแยกแยะประพจน์ออกจากประเภทของวัตถุที่ถูกระบุปริมาณ ตรรกะลำดับสูงกว่าใช้วิธีการที่แตกต่างออกไปและมีประพจน์เพียงประเภทเดียวเท่านั้น ตัวระบุปริมาณมีขอบเขตของการระบุปริมาณเป็นประพจน์ประเภทเดียวกัน ดังที่สะท้อนให้เห็นในกฎการสร้าง:

${\displaystyle {\cfrac {\begin{matrix}{\cfrac {}{p:{\mathcal {F}}}}{\hbox{ u}}\\\vdots \\A:{\mathcal {F}}\\\end{matrix}}{\forall p.A:{\mathcal {F}}}}\;\forall _{F^{u}}\qquad \qquad {\cfrac {\begin{matrix}{\cfrac {}{p:{\mathcal {F}}}}{\hbox{ u}}\\\vdots \\A:{\mathcal {F}}\\\end{matrix}}{\exists p.A:{\mathcal {F}}}}\;\exists _{F^{u}}}$

การอธิบายรูปแบบการแนะนำและการกำจัดสำหรับตรรกะลำดับสูงนั้นอยู่นอกเหนือขอบเขตของบทความนี้ เป็นไปได้ที่จะมีตรรกะที่อยู่ระหว่างตรรกะลำดับแรกและตรรกะลำดับสูง ตัวอย่างเช่นตรรกะลำดับที่สองมีประพจน์สองประเภท ประเภทหนึ่งกำหนดปริมาณของพจน์ และประเภทที่สองกำหนดปริมาณของประพจน์ประเภทแรก

การนำเสนอการอนุมานเชิงธรรมชาติที่ผ่านมานั้นมุ่งเน้นไปที่ธรรมชาติของประพจน์โดยไม่ได้ให้คำจำกัดความอย่างเป็นทางการของการพิสูจน์เพื่อทำให้แนวคิดเรื่องการพิสูจน์เป็นทางการมากขึ้น เราจึงปรับเปลี่ยนการนำเสนอการอนุมานเชิงสมมติฐานเล็กน้อย เรากำหนดตัวแปรการพิสูจน์ (จากเซตตัวแปรที่นับได้V ) ให้กับส่วนนำ และตกแต่งส่วนตามด้วยการพิสูจน์จริง ส่วนนำหรือสมมติฐานจะถูกแยกออกจากส่วนตามโดยใช้ตัวคั่น (⊢) การปรับเปลี่ยนนี้บางครั้งเรียกว่าสมมติฐานเฉพาะที่แผนภาพต่อไปนี้สรุปการเปลี่ยนแปลงดังกล่าว

──── คุณ1 ──── คุณ2 ... ──── คุณ J 1 J 2 J n ⋮ เจ 

คุณ1 :J 1 , คุณ2 :J 2 , ..., คุณ: J n ⊢ J 

ชุดสมมติฐานจะถูกเขียนแทนด้วย Γ เมื่อองค์ประกอบที่แน่นอนของสมมติฐานเหล่านั้นไม่สำคัญ เพื่อให้การพิสูจน์ชัดเจนขึ้น เราจะเปลี่ยนจากการตัดสินที่ไม่มีการพิสูจน์ " A " ไปเป็นการตัดสินว่า "π เป็นการพิสูจน์ของ (A) " ซึ่งเขียนในเชิงสัญลักษณ์ว่า "π : A " ตามแนวทางมาตรฐาน การพิสูจน์จะถูกกำหนดด้วยกฎการสร้างของตัวเองสำหรับการตัดสินว่า "π พิสูจน์ได้ " การพิสูจน์ที่ง่ายที่สุดคือการใช้สมมติฐานที่มีป้ายกำกับ ในกรณีนี้ หลักฐานคือป้ายกำกับนั้นเอง

u ∈ V ─────── proof-F หลักฐานของคุณ 

──────────────────── hyp u:A ⊢ u : A 

เรามาทบทวนตัวเชื่อมบางตัวพร้อมบทพิสูจน์ที่ชัดเจนกันอีกครั้ง สำหรับการเชื่อมประโยค เราจะดูที่กฎการแนะนำ ∧I เพื่อค้นหารูปแบบของบทพิสูจน์การเชื่อมประโยค: บทพิสูจน์เหล่านั้นจะต้องเป็นคู่ของบทพิสูจน์ของตัวเชื่อมทั้งสอง ดังนั้น:

π 1พิสูจน์ π 2พิสูจน์ ─────────────────── pair-F (π 1 , π 2 ) พิสูจน์ 

Γ ⊢ π 1  : A Γ ⊢ π 2  : B ──────────────────────── ∧ฉัน Γ ⊢ (π 1 , π 2 ) : A ∧ B 

กฎการกำจัด ∧E ₁และ ∧E ₂เลือกส่วนประกอบด้านซ้ายหรือด้านขวา ดังนั้นการพิสูจน์จึงเป็นการฉายภาพคู่หนึ่ง คือ การฉายภาพครั้งแรก ( fst ) และการฉายภาพครั้งที่สอง ( snd )

การพิสูจน์ π ─────────── fst -F fst π พิสูจน์ 

Γ ⊢ π : A ∧ B ───────────── ∧E 1 Γ ⊢ fst π : A 

การพิสูจน์ π ─────────── snd -F snd π proof 

Γ ⊢ π : A ∧ B ───────────── ∧E 2 Γ ⊢ snd π : B 

สำหรับการอนุมาน รูปแบบการแนะนำจะระบุตำแหน่งหรือผูก สมมติฐานที่ เขียน โดยใช้ λ ซึ่งสอดคล้องกับป้ายกำกับที่ถูกปลดออก ในกฎ "Γ, u : A " หมายถึงชุดของสมมติฐาน Γ พร้อมกับสมมติฐานเพิ่มเติมu

การพิสูจน์ π ──────────── แล-F λu. π พิสูจน์ 

Γ, u:A ⊢ π : B ──────────────── ⊃ฉัน Γ ⊢ λu. π : A ⊃ B 

π 1พิสูจน์ π 2พิสูจน์ ────────────────── app-F π 1 π 2พิสูจน์ 

Γ ⊢ π 1  : A ⊃ B Γ ⊢ π 2  : A ─────────────────────────── ⊃E Γ ⊢ π 1 π 2  : B 

เมื่อมีบทพิสูจน์ที่แสดงไว้อย่างชัดเจน เราสามารถจัดการและให้เหตุผลเกี่ยวกับบทพิสูจน์ได้ การดำเนินการที่สำคัญในบทพิสูจน์คือการแทนที่ข้อสมมติในบทพิสูจน์หนึ่งด้วยบทพิสูจน์อื่น ซึ่งโดยทั่วไปเรียกว่าทฤษฎีบทการแทนที่และสามารถพิสูจน์ได้โดยการอุปมานตามความลึก (หรือโครงสร้าง) ของการตัดสินครั้งที่สอง

ถ้า Γ ⊢ π ₁  : A และ Γ, u : A ⊢ π 2 : B แล้ว_Γ  ⊢ [ π 1 _/ u ] π ₂  : B

ที่ผ่านมา คำตัดสิน "Γ ⊢ π : A " มีการตีความในเชิงตรรกะล้วนๆ ในทฤษฎีประเภท (Type Theory ) มุมมองเชิงตรรกะจะถูกแทนที่ด้วยมุมมองเชิงคำนวณของวัตถุมากขึ้น ข้อเสนอในเชิงตรรกะจะถูกมองว่าเป็นประเภทและการพิสูจน์จะถูกมองว่าเป็นโปรแกรมในแคลคูลัสแลมบ์ดาดังนั้น การตีความของ "π : A " คือ " โปรแกรม π มีประเภทA " ตัวเชื่อมทางตรรกะก็ได้รับการตีความที่แตกต่างกันเช่นกัน การเชื่อมโยง (Conjunction) ถูกมองว่าเป็นผลคูณ (×) การบ่งชี้ (Implication) ถูกมองว่าเป็นลูกศร ฟังก์ชัน (→) เป็นต้น อย่างไรก็ตาม ความแตกต่างเหล่านี้เป็นเพียงแค่รูปลักษณ์ภายนอกเท่านั้น ทฤษฎีประเภทมีการนำเสนอการอนุมานตามธรรมชาติในแง่ของกฎการสร้าง การแนะนำ และการกำจัด อันที่จริง ผู้อ่านสามารถสร้างสิ่งที่เรียกว่าทฤษฎีประเภทแบบง่าย ขึ้นมาใหม่ได้ง่ายๆ จากส่วนก่อนหน้า

ความแตกต่างระหว่างตรรกศาสตร์และทฤษฎีประเภทนั้นอยู่ที่การเปลี่ยนจุดสนใจจากประเภท (ประพจน์) ไปยังโปรแกรม (การพิสูจน์) เป็นหลัก ทฤษฎีประเภทสนใจในเรื่องความสามารถในการแปลงหรือลดรูปของโปรแกรมเป็นหลัก สำหรับทุกประเภท จะมีโปรแกรมมาตรฐานของประเภทนั้นที่ไม่สามารถลดรูปได้ ซึ่งเรียกว่ารูปแบบมาตรฐานหรือค่ามาตรฐานหากทุกโปรแกรมสามารถลดรูปเป็นรูปแบบมาตรฐานได้ ทฤษฎีประเภทนั้นจะเรียกว่าเป็นแบบมาตรฐาน (หรือแบบมาตรฐานอ่อน ) หากรูปแบบมาตรฐานมีเพียงหนึ่งเดียว ทฤษฎีนั้นจะเรียกว่าเป็นแบบมาตรฐานเข้ม ความสามารถในการทำให้เป็นมาตรฐานเป็นคุณลักษณะที่หายากของทฤษฎีประเภทที่ไม่ใช่แบบธรรมดาส่วนใหญ่ ซึ่งแตกต่างอย่างมากจากโลกของตรรกศาสตร์ (โปรดจำไว้ว่าการอนุมานเชิงตรรกศาสตร์เกือบทุกอย่างมีการอนุมานปกติที่เทียบเท่ากัน) เพื่ออธิบายเหตุผลโดยคร่าวๆ: ในทฤษฎีประเภทที่ยอมรับนิยามแบบเรียกซ้ำ เป็นไปได้ที่จะเขียนโปรแกรมที่ไม่ลดรูปเป็นค่าใดๆ เลย โปรแกรมวนซ้ำดังกล่าวโดยทั่วไปสามารถกำหนดประเภทใดก็ได้ โดยเฉพาะอย่างยิ่ง โปรแกรมวนซ้ำมีประเภท ⊥ แม้ว่าจะไม่มีการพิสูจน์เชิงตรรกศาสตร์ของ "⊥" ก็ตาม ด้วยเหตุนี้ รูป แบบ ที่ว่า ข้อเสนอเป็นประเภท การพิสูจน์เป็นโปรแกรมจึงใช้ได้เพียงทิศทางเดียวเท่านั้น หรืออาจใช้ไม่ได้เลย กล่าวคือ การตีความทฤษฎีประเภทเป็นตรรกะโดยทั่วไปจะให้ตรรกะที่ไม่สอดคล้องกัน

เช่นเดียวกับตรรกศาสตร์ ทฤษฎีประเภทก็มีส่วนขยายและรูปแบบต่างๆ มากมาย รวมถึงเวอร์ชันลำดับที่หนึ่งและลำดับที่สูงกว่า สาขาหนึ่งที่เรียกว่าทฤษฎีประเภทแบบพึ่งพา (Dependent Type Theory) ถูกนำไปใช้ในระบบ พิสูจน์ด้วยคอมพิวเตอร์หลายระบบ ทฤษฎีประเภทแบบพึ่งพาอนุญาตให้ตัวบ่งปริมาณครอบคลุมโปรแกรมเองได้ ประเภทที่มีตัวบ่งปริมาณเหล่านี้เขียนเป็น Π และ Σ แทนที่จะเป็น ∀ และ ∃ และมีกฎการสร้างดังต่อไปนี้:

Γ ⊢ ประเภท A Γ, x:A ⊢ ประเภท B ───────────────────────────── Π-F Γ ⊢ Πx:A. ประเภท B 

Γ ⊢ ประเภท A Γ, x:A ⊢ ประเภท B ──────────────────────────── Σ-F Γ ⊢ Σx:A. ประเภท B 

ประเภทเหล่านี้เป็นการสรุปโดยทั่วไปของประเภทลูกศรและประเภทผลคูณ ตามลำดับ ดังที่เห็นได้จากกฎการแนะนำและการกำจัดของพวกมัน

Γ, x:A ⊢ π : B ─────────────────── ΠI Γ ⊢ λx. π : Πx:A. B 

Γ ⊢ π 1  : Πx:A. บี Γ ⊢ π 2  : ก ───────────────────────────── ΠE Γ ⊢ π 1 π 2  : [π 2 /x] บ 

Γ ⊢ π 1  : A Γ, x:A ⊢ π 2  : B ──────────────────────────── ΣI Γ ⊢ (π 1 , π 2 ) : Σx:A. บี 

Γ ⊢ π : Σx:A. B ──────────────── ΣE 1 Γ ⊢ fst π : A 

Γ ⊢ π : Σx:A. B ──────────────────────── ΣE 2 Γ ⊢ snd π : [ fst π/x] B 

ทฤษฎีประเภทแบบพึ่งพา (Dependent type theory) ในรูปแบบทั่วไปนั้นทรงพลังมาก: มันสามารถแสดงคุณสมบัติเกือบทุกอย่างของโปรแกรมได้โดยตรงในประเภทของโปรแกรมนั้นเอง ความทั่วไปนี้มาพร้อมกับราคาที่สูง — ไม่ว่าจะเป็นการตรวจสอบประเภทที่ไม่สามารถตัดสินได้ ( ทฤษฎีประเภทแบบขยาย ) หรือการให้เหตุผลแบบขยายทำได้ยากขึ้น ( ทฤษฎีประเภทแบบเจาะจง ) ด้วยเหตุนี้ ทฤษฎีประเภทแบบพึ่งพาบางทฤษฎีจึงไม่อนุญาตให้มีการกำหนดปริมาณเหนือโปรแกรมใดๆ แต่จะจำกัดเฉพาะโปรแกรมที่มี โดเมนดัชนีที่ตัดสินได้เช่น จำนวนเต็ม สตริง หรือโปรแกรมเชิงเส้น

เนื่องจากทฤษฎีประเภทแบบพึ่งพาอนุญาตให้ประเภทพึ่งพาโปรแกรมได้ คำถามที่เกิดขึ้นตามธรรมชาติคือ เป็นไปได้หรือไม่ที่โปรแกรมจะพึ่งพาประเภท หรือการผสมผสานอื่นๆ มีคำตอบมากมายสำหรับคำถามดังกล่าว แนวทางที่นิยมในทฤษฎีประเภทคือการอนุญาตให้โปรแกรมถูกกำหนดปริมาณเหนือประเภท หรือที่เรียกว่าโพลีมอร์ฟิซึมแบบพารามิเตอร์ซึ่งมีอยู่สองประเภทหลัก: หากประเภทและโปรแกรมแยกจากกัน จะได้ระบบที่มีพฤติกรรมที่ดีกว่าเล็กน้อย เรียกว่าโพลีมอร์ฟิซึมแบบทำนายได้หากความแตกต่างระหว่างโปรแกรมและประเภทไม่ชัดเจน จะได้สิ่งที่เทียบเคียงได้กับตรรกะลำดับสูงในทางทฤษฎีประเภท หรือที่เรียกว่า โพลีมอร์ฟิซึมแบบ ไม่ทำนายได้มีการพิจารณาการผสมผสานต่างๆ ของการพึ่งพาและโพลีมอร์ฟิซึมในวรรณกรรม ซึ่งที่โด่งดังที่สุดคือแลมบ์ดาคิวบ์ของHenk Barendregt

การบรรจบกันของตรรกศาสตร์และทฤษฎีประเภทเป็นพื้นที่วิจัยที่กว้างขวางและคึกคัก ตรรกศาสตร์ใหม่มักถูกกำหนดรูปแบบอย่างเป็นทางการในบริบทของทฤษฎีประเภททั่วไป ซึ่งเรียกว่ากรอบตรรกะกรอบตรรกะสมัยใหม่ที่เป็นที่นิยม เช่นแคลคูลัสของการสร้างและLFนั้นอิงตามทฤษฎีประเภทพึ่งพาอันดับสูง โดยมีการแลกเปลี่ยนข้อดีข้อเสียต่างๆ ในแง่ของความสามารถในการตัดสินใจและพลังในการแสดงออก กรอบตรรกะเหล่านี้มักถูกกำหนดให้เป็นระบบการอนุมานตามธรรมชาติ ซึ่งเป็นเครื่องพิสูจน์ถึงความอเนกประสงค์ของแนวทางการอนุมานตามธรรมชาติ

เพื่อความง่าย ตรรกะที่นำเสนอมาจนถึงตอนนี้เป็น ตรรกะ แบบสัญชาตญาณตรรกะแบบคลาสสิกขยายตรรกะแบบสัญชาตญาณด้วยสัจพจน์ เพิ่มเติม หรือหลักการของสิ่งที่ไม่รวมอยู่ตรงกลาง :

สำหรับข้อเสนอใดๆ p ข้อเสนอ p ∨ ¬p เป็นจริง

ข้อความนี้ไม่ได้แสดงให้เห็นอย่างชัดเจนว่าเป็นทั้งการแนะนำหรือการกำจัด อันที่จริง มันเกี่ยวข้องกับตัวเชื่อมสองตัวที่แตกต่างกัน การวิเคราะห์ดั้งเดิมของเกนท์เซนเกี่ยวกับกริยาช่องกลางที่ถูกยกเว้นได้กำหนดสูตรหนึ่งในสามสูตรต่อไปนี้ (ซึ่งเทียบเท่ากัน) ซึ่งมีอยู่แล้วในรูปแบบที่คล้ายคลึงกันในระบบของฮิลเบิร์ตและเฮย์ติง :

────────────── XM 1 A ∨ ¬A 

¬¬A ────────── XM 2 เอ 

──────── u ¬A ⋮ p ────── XM 3 u, p เอ 

(XM ₃ก็คือ XM ₂ที่แสดงในรูปของ E นั่นเอง) การจัดการกับรูปแบบกึ่งกลางที่ถูกยกเว้นนี้ นอกจากจะขัดกับมุมมองของผู้ที่ยึดมั่นในความบริสุทธิ์แล้ว ยังก่อให้เกิดความซับซ้อนเพิ่มเติมในการกำหนดรูปแบบปกติอีกด้วย

วิธีการแก้ปัญหาการอนุมานเชิงธรรมชาติแบบคลาสสิกที่น่าพอใจกว่าในแง่ของกฎการแนะนำและการกำจัดเพียงอย่างเดียว ได้รับการเสนอครั้งแรกโดยParigotในปี 1992 ในรูปแบบของแคลคูลัสแลมบ์ดา แบบคลาสสิกที่ เรียกว่าλμแนวคิดหลักของวิธีการของเขาคือการแทนที่การตัดสินที่เน้นความจริงAด้วยแนวคิดแบบคลาสสิกมากขึ้น ซึ่งชวนให้นึกถึงแคลคูลัสลำดับ : ในรูปแบบเฉพาะที่ แทนที่จะใช้ Γ ⊢ Aเขาใช้ Γ ⊢ Δ โดยที่ Δ เป็นชุดของประพจน์ที่คล้ายกับ Γ Γ ถูกมองว่าเป็นการเชื่อมโยง และ Δ เป็นการแยก โครงสร้างนี้โดยพื้นฐานแล้วยกมาจากแคลคูลัสลำดับแบบคลาสสิก โดยตรง แต่ความแปลกใหม่ใน λμ คือการให้ความหมายเชิงคำนวณแก่การพิสูจน์การอนุมานเชิงธรรมชาติแบบคลาสสิกในแง่ของ กลไก callccหรือ throw/catch ที่พบในLISPและภาษาที่สืบทอดมา (ดูเพิ่มเติม: การควบคุมชั้นหนึ่ง )

ส่วนขยายที่สำคัญอีกประการหนึ่งคือสำหรับตรรกะเชิงโมดอลและตรรกะอื่นๆ ที่ต้องการมากกว่าการตัดสินความจริงขั้นพื้นฐาน ตรรกะเหล่านี้ได้รับการอธิบายครั้งแรกสำหรับตรรกะเชิงโมดอลแบบอาเลธิกS4และS5ในรูปแบบการอนุมานตามธรรมชาติโดยPrawitzในปี 1965 ^{[ 5 ]}และตั้งแต่นั้นมาก็มีผลงานที่เกี่ยวข้องจำนวนมาก ตัวอย่างง่ายๆ คือ ตรรกะเชิงโมดอล S4 ต้องการการตัดสินใหม่หนึ่งอย่างคือ " ถูกต้อง " ซึ่งเป็นแบบจำแนกประเภทเกี่ยวกับความจริง:

ถ้า "A" (เป็นจริง) โดยไม่มีข้อสมมติใดๆ ว่า "B" (เป็นจริง) แล้ว "A ใช้ได้"

การตัดสินเชิงหมวดหมู่นี้ถูกทำให้เป็นส่วนประกอบภายในในรูปของตัวเชื่อมเอกภาค ◻ A (อ่านว่า " จำเป็นต้องเป็น A ") โดยมีกฎการแนะนำและการกำจัดดังต่อไปนี้:

ถูกต้อง ──────── ◻ฉัน ◻ เอ 

◻ เอ ──────── ◻E เอ 

โปรดสังเกตว่าข้อสมมติฐาน " A ถูกต้อง " ไม่มีกฎเกณฑ์ที่กำหนดไว้ตายตัว แต่จะใช้คำจำกัดความเชิงหมวดหมู่ของความถูกต้องแทน วิธีการนี้จะชัดเจนยิ่งขึ้นในรูปแบบเฉพาะที่เมื่อสมมติฐานมีความชัดเจน เราเขียน "Ω;Γ ⊢ A " โดยที่ Γ ประกอบด้วยสมมติฐานที่เป็นจริงเช่นเดิม และ Ω ประกอบด้วยสมมติฐานที่ถูกต้อง ทางด้านขวามีเพียงการตัดสินเดียวคือ " A " ความถูกต้องไม่จำเป็นในที่นี้เนื่องจาก "Ω ⊢ A ถูกต้อง " ตามคำจำกัดความแล้วเหมือนกับ "Ω;⋅ ⊢ A " รูปแบบการนำเสนอและการกำจัดจึงเป็นดังนี้:

Ω;⋅ ⊢ π : A ─────────────────── ◻ฉัน Ω;⋅ ⊢ กล่อง π : ◻ A 

Ω;Γ ⊢ π : ◻ A ────────────────────── ◻E Ω;Γ ⊢ unbox π : A 

สมมติฐานเชิงโมดอลมีกฎสมมติฐานและทฤษฎีบทการแทนที่ในรูปแบบเฉพาะของตนเอง

─────────────────────────────── valid-hyp Ω, u: (ถูกต้อง) ; Γ ⊢ u : A 

ถ้า Ω;⋅ ⊢ π ₁  : A และ Ω, u : ( A valid ) ; Γ ⊢ π ₂  : C แล้ว Ω ; Γ ⊢ [π ₁ / u ] π ₂  : C .

กรอบแนวคิดการแยกการตัดสินออกเป็นกลุ่มสมมติฐานที่แตกต่างกัน ซึ่งเรียกอีกอย่างว่า บริบท แบบหลายโซนหรือ แบบ หลายตัวเลือกนั้น มีประสิทธิภาพและขยายได้มาก มีการนำไปประยุกต์ใช้กับตรรกะเชิงโมดอลหลายประเภท รวมถึง ตรรกะ เชิงเส้นและตรรกะเชิงโครงสร้างย่อย อื่นๆ อย่างไรก็ตาม ระบบตรรกะเชิงโมดอลเพียงไม่กี่ระบบเท่านั้นที่สามารถทำให้เป็นทางการได้โดยตรงด้วยการอนุมานตามธรรมชาติ เพื่อให้ได้ลักษณะเฉพาะเชิงทฤษฎีการพิสูจน์ของระบบเหล่านี้ จึงจำเป็นต้องมีการขยายเพิ่มเติม เช่น การติดป้ายกำกับ หรือระบบการอนุมานเชิงลึก

การเพิ่มป้ายกำกับให้กับสูตรช่วยให้สามารถควบคุมเงื่อนไขที่กฎใช้ได้อย่างละเอียดมากขึ้น ทำให้สามารถนำเทคนิคที่ยืดหยุ่นกว่าของตารางวิเคราะห์มาใช้ได้ ดังเช่นที่ได้ทำในกรณีของการอนุมานแบบมีป้ายกำกับ ป้ายกำกับยังช่วยให้สามารถตั้งชื่อโลกในความหมายแบบคริปเคได้ซิมป์สัน (1994)นำเสนอเทคนิคที่มีอิทธิพลในการแปลงเงื่อนไขเฟรมของตรรกะเชิงโมดอลในความหมายแบบคริปเคให้เป็นกฎการอนุมานในรูปแบบการอนุมานตามธรรมชาติของตรรกะแบบผสมสตู พพา ( 2004)สำรวจการประยุกต์ใช้ทฤษฎีการพิสูจน์หลายอย่าง เช่น ไฮเปอร์ซีเควนต์ของอัฟรอนและพอตทิงเจอร์และตรรกะการแสดงผล ของเบลแนป กับตรรกะเชิงโมดอลเช่น S5 และ B

แคลคูลัสลำดับเป็นทางเลือกหลักแทนการอนุมานตามธรรมชาติในฐานะพื้นฐานของตรรกะทางคณิตศาสตร์ในการอนุมานตามธรรมชาติ การไหลของข้อมูลเป็นแบบสองทิศทาง: กฎการกำจัดจะส่งข้อมูลลงด้านล่างโดยการแยกส่วน และกฎการแนะนำจะส่งข้อมูลขึ้นด้านบนโดยการประกอบ ดังนั้น การพิสูจน์โดยการอนุมานตามธรรมชาติจึงไม่มีการอ่านแบบจากล่างขึ้นบนหรือจากบนลงล่างอย่างแท้จริง ทำให้ไม่เหมาะสมสำหรับการทำงานอัตโนมัติในการค้นหาการพิสูจน์ เพื่อแก้ไขข้อเท็จจริงนี้Gentzen ได้เสนอ แคลคูลัสลำดับของเขาในปี 1935 แม้ว่าในตอนแรกเขาตั้งใจให้เป็นเครื่องมือทางเทคนิคเพื่อชี้แจงความสอดคล้องของตรรกะภาคแสดง Kleene ในหนังสือสำคัญของเขาในปี 1952 เรื่อง Introduction to Metamathematicsได้ให้สูตรแรกของแคลคูลัสลำดับในรูปแบบสมัยใหม่^{[ 44 ]}

ในแคลคูลัสลำดับ (sequent calculus) กฎการอนุมานทั้งหมดมีการตีความจากล่างขึ้นบนอย่างแท้จริง กฎการอนุมานสามารถใช้ได้กับองค์ประกอบทั้งสองด้านของประตูหมุน (เพื่อแยกความแตกต่างจากการอนุมานเชิงธรรมชาติ บทความนี้ใช้ลูกศรคู่ ⇒ แทนเครื่องหมายลูกศรชี้ไปทางขวา ⊢ สำหรับลำดับ) กฎการแนะนำของการอนุมานเชิงธรรมชาติถือเป็นกฎทางขวาในแคลคูลัสลำดับ และมีโครงสร้างที่คล้ายคลึงกันมาก ในทางกลับกัน กฎการกำจัดจะกลายเป็นกฎทางซ้ายในแคลคูลัสลำดับ ยกตัวอย่างเช่น การเชื่อมแบบ "หรือ" (disjunction) กฎทางขวานั้นคุ้นเคยกันดี:

Γ ⇒ A ───────── ∨R 1 Γ ⇒ A ∨ B 

Γ ⇒ B ───────── ∨R 2 Γ ⇒ A ∨ B 

ทางด้านซ้าย:

Γ, u:A ⇒ C Γ, v:B ⇒ C ─────────────────────────── ∨L Γ, w: (A ∨ B) ⇒ C 

โปรดระลึกถึงกฎ ∨E ของการอนุมานเชิงธรรมชาติในรูปแบบเฉพาะที่:

Γ ⊢ A ∨ B Γ, u:A ⊢ C Γ, v:B ⊢ C ─────────────────────────────────────── ∨E Γ ⊢ C 

ข้อเสนอA ∨ Bซึ่งเป็นผลสืบเนื่องของข้อตั้งต้นใน ∨E จะกลายเป็นสมมติฐานของข้อสรุปในกฎซ้าย ∨L ดังนั้น กฎซ้ายจึงอาจมองได้ว่าเป็นกฎการกำจัดแบบกลับด้านชนิดหนึ่ง ข้อสังเกตนี้สามารถแสดงให้เห็นได้ดังนี้:

────── hyp | | กฎการคัดออก | ↓ ───────────────────── ↑↓ พบปะ ↑ | | กฎเบื้องต้น | บทสรุป

─────────────────────────── เริ่ม ↑ ↑ || | กฎซ้าย | กฎขวา || บทสรุป

ในแคลคูลัสลำดับ (sequent calculus) กฎด้านซ้ายและด้านขวาจะถูกดำเนินการไปพร้อมกันจนกว่าจะถึงลำดับเริ่มต้น (initial sequent ) ซึ่งสอดคล้องกับจุดบรรจบกันของกฎการกำจัดและกฎการแนะนำในอนุมานเชิงธรรมชาติ (natural deduction) กฎเริ่มต้นเหล่านี้ดูคล้ายกับกฎสมมติฐานของอนุมานเชิงธรรมชาติ แต่ในแคลคูลัสลำดับนั้น กฎเหล่านี้อธิบายถึงการสลับตำแหน่งหรือการจับมือกันของประพจน์ด้านซ้ายและด้านขวา:

────────── เริ่มต้น Γ, u:A ⇒ A 

ความสอดคล้องกันระหว่างแคลคูลัสลำดับและการอนุมานเชิงธรรมชาติคือทฤษฎีบทความถูกต้องและความสมบูรณ์สองข้อ ซึ่งทั้งสองข้อสามารถพิสูจน์ได้โดยใช้การให้เหตุผลแบบอุปนัย

ความถูกต้องของ ⇒ เมื่อเทียบกับ ⊢

ถ้า Γ ⇒ Aแล้วΓ ⊢ A

ความสมบูรณ์ของ ⇒ เมื่อเทียบกับ ⊢

ถ้า Γ ⊢ Aแล้วΓ ⇒ A

จากทฤษฎีบทเหล่านี้เห็นได้ชัดว่าแคลคูลัสลำดับไม่เปลี่ยนแปลงแนวคิดเรื่องความจริง เพราะชุดของประพจน์ยังคงเป็นจริงเช่นเดิม ดังนั้น เราจึงสามารถใช้วัตถุพิสูจน์แบบเดียวกันกับที่เคยใช้มาก่อนในการพิสูจน์ด้วยแคลคูลัสลำดับได้ ตัวอย่างเช่น พิจารณาการเชื่อมโยง กฎทางขวานั้นแทบจะเหมือนกับกฎการแนะนำ

Γ ⇒ π 1  : A Γ ⇒ π 2  : B ────────────────────────── ∧R Γ ⇒ (π 1 , π 2 ) : A ∧ B 

Γ ⊢ π 1  : A Γ ⊢ π 2  : B ──────────────────────── ∧ฉัน Γ ⊢ (π 1 , π 2 ) : A ∧ B 

อย่างไรก็ตาม กฎทางซ้ายมือมีการแทนที่เพิ่มเติมบางอย่างที่ไม่เกิดขึ้นในกฎการกำจัดที่เกี่ยวข้อง

Γ, u:A ⇒ π : C ──────────────────────────────── ∧L 1 Γ, v: (A ∧ B) ⇒ [ fst v/u] π : C 

Γ ⊢ π : A ∧ B ───────────── ∧E 1 Γ ⊢ fst π : A 

Γ, u:B ⇒ π : C ──────────────────────────────── ∧L 2 Γ, v: (A ∧ B) ⇒ [ snd v/u] π : C 

Γ ⊢ π : A ∧ B ───────────── ∧E 2 Γ ⊢ snd π : B 

ดังนั้น รูปแบบการพิสูจน์ที่สร้างขึ้นในแคลคูลัสลำดับจึงค่อนข้างแตกต่างจากการพิสูจน์โดยการอนุมานตามธรรมชาติ แคลคูลัสลำดับสร้างการพิสูจน์ในสิ่งที่เรียกว่า รูปแบบ β-ปกติ η-ยาวซึ่งสอดคล้องกับการแสดงแบบแคนอนิกของรูปแบบปกติของการพิสูจน์โดยการอนุมานตามธรรมชาติ หากพยายามอธิบายการพิสูจน์เหล่านี้โดยใช้การอนุมานตามธรรมชาติเอง จะได้สิ่งที่เรียกว่าแคลคูลัสการแทรก (ซึ่งอธิบายครั้งแรกโดยจอห์น ไบรน์ส) ซึ่งสามารถใช้เพื่อกำหนดแนวคิดของรูปแบบปกติสำหรับการอนุมานตามธรรมชาติ ได้อย่างเป็นทางการ

ทฤษฎีบทการแทนที่ของการอนุมานเชิงธรรมชาติมีรูปแบบเป็นกฎเชิงโครงสร้างหรือทฤษฎีบทเชิงโครงสร้างที่เรียกว่า " การตัด"ในแคลคูลัสลำดับ

ถ้า Γ ⇒ π ₁  : A และ Γ , u : A ⇒ π ₂  : Cแล้วΓ ⇒ [π ₁ /u] π ₂  : C

ในตรรกศาสตร์ส่วนใหญ่ที่มีพฤติกรรมที่ดี กฎ "ตัด" (cut) ไม่จำเป็นต้องใช้เป็นกฎการอนุมาน แม้ว่าจะยังคงพิสูจน์ได้ว่าเป็นทฤษฎีบทเสริมก็ตาม ความไม่จำเป็นของกฎ "ตัด" มักถูกนำเสนอในรูปของกระบวนการคำนวณที่เรียกว่าการกำจัด "ตัด" (cut elimination ) สิ่งนี้มีประโยชน์อย่างน่าสนใจสำหรับการอนุมานเชิงธรรมชาติ โดยปกติแล้วการพิสูจน์คุณสมบัติบางอย่างโดยตรงในการอนุมานเชิงธรรมชาตินั้นยุ่งยากมากเนื่องจากจำนวนกรณีที่ไม่จำกัด ตัวอย่างเช่น ลองพิจารณาการแสดงว่าข้อเสนอที่กำหนดนั้นไม่สามารถพิสูจน์ได้ในการอนุมานเชิงธรรมชาติ การให้เหตุผลแบบอุปนัยอย่างง่ายจะล้มเหลวเนื่องจากกฎเช่น ∨E หรือ E ซึ่งสามารถนำเสนอข้อเสนอใดๆ ก็ได้ อย่างไรก็ตาม เรารู้ว่าแคลคูลัสลำดับนั้นสมบูรณ์เมื่อเทียบกับการอนุมานเชิงธรรมชาติ ดังนั้นจึงเพียงพอที่จะแสดงให้เห็นถึงความไม่สามารถพิสูจน์ได้ในแคลคูลัสลำดับ ทีนี้ ถ้า "ตัด" ไม่สามารถใช้เป็นกฎการอนุมานได้ กฎลำดับทั้งหมดจะนำเสนอตัวเชื่อมทางด้านขวาหรือด้านซ้าย ดังนั้นความลึกของการอนุมานลำดับจึงถูกจำกัดอย่างสมบูรณ์โดยตัวเชื่อมในข้อสรุปสุดท้าย ดังนั้น การแสดงให้เห็นว่าพิสูจน์ไม่ได้จึงง่ายกว่ามาก เพราะมีเพียงจำนวนกรณีที่จำกัดให้พิจารณา และแต่ละกรณีประกอบด้วยข้อเสนอย่อยของข้อสรุปทั้งหมด ตัวอย่างง่ายๆ คือ ทฤษฎี บทความสอดคล้องทั่วโลก : "⋅ ⊢ ⊥" พิสูจน์ไม่ได้ ในเวอร์ชันแคลคูลัสลำดับ สิ่งนี้เป็นจริงอย่างชัดเจน เพราะไม่มีกฎใดที่สามารถมี "⋅ ⇒ ⊥" เป็นข้อสรุปได้! นักทฤษฎีการพิสูจน์มักชอบทำงานกับสูตรแคลคูลัสลำดับแบบไร้การตัดเนื่องจากคุณสมบัติดังกล่าว

• อินเดรย์ชัค, อันเดรย์. "การอนุมานเชิงธรรมชาติ" . สารานุกรมปรัชญาออนไลน์. สืบค้นเมื่อ4 พฤษภาคม 2025 .
• ลาโบเรโอ, แดเนียล เคลเมนเต (สิงหาคม 2547) “ความรู้เบื้องต้นเกี่ยวกับการหักตามธรรมชาติ” (PDF) .
• "Domino On Acid" . สืบค้นเมื่อ 10 ธันวาคม 2023 . การอนุมานเชิงธรรมชาติที่แสดงออกมาในรูปแบบเกมโดมิโน
• เพลเลเทียร์, ฟรานซิส เจฟฟรีย์. "ประวัติของตำราตรรกศาสตร์เชิงอนุมานและตรรกศาสตร์เบื้องต้น" (PDF )
• บทความเรื่อง "ระบบการอนุมานตามธรรมชาติในตรรกศาสตร์"โดย Pelletier, Francis Jeffry และ Hazen, Allen ในสารานุกรมปรัชญาแห่งสแตนฟอร์ด ฉบับวันที่ 29 ตุลาคม 2021
• เลวี, มิเชล. "ตัวพิสูจน์เชิงประพจน์" .