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

แคลคูลัสลำดับ (Sequent calculus) เป็นหนึ่งในรูปแบบแคลคูลัสพิสูจน์ ที่มีอยู่หลายรูปแบบ สำหรับการแสดงข้อโต้แย้งเชิงตรรกะทีละบรรทัด

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

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

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

ในทฤษฎีการพิสูจน์และตรรกศาสตร์ทางคณิตศาสตร์แคลคูลัสลำดับเป็นกลุ่มของระบบที่เป็นทางการที่ใช้รูปแบบการอนุมานและคุณสมบัติที่เป็นทางการบางอย่างร่วมกัน ระบบแคลคูลัสลำดับแรกLKและLJได้รับการแนะนำในปี 1934/1935 โดย Gerhard Gentzen ^{[ 1 ]}ในฐานะเครื่องมือสำหรับการศึกษาการอนุมานตามธรรมชาติในตรรกศาสตร์ลำดับที่หนึ่ง (ใน เวอร์ชัน คลาสสิกและ แบบ สัญชาตญาณตามลำดับ) สิ่งที่ Gentzen เรียกว่า "ทฤษฎีบทหลัก" ( Hauptsatz ) เกี่ยวกับ LK และ LJ คือทฤษฎีบทการกำจัดส่วนตัด [ ^{2 ] [ 3 ]} ซึ่งเป็นผลลัพธ์ที่มี ผลกระทบเชิงอภิปรัชญาที่กว้างไกล รวมถึง ความสอดคล้อง Gentzen ยังได้แสดงให้เห็นถึงพลังและความยืดหยุ่นของ ^{เทคนิค}นี้อีกไม่กี่ปีต่อมา โดยใช้การโต้แย้งการกำจัดส่วนตัดเพื่อให้การพิสูจน์ ( อนันต์ ) ของความสอดคล้องของเลขคณิต Peanoซึ่งเป็นการตอบสนองที่น่าประหลาดใจต่อทฤษฎีบทความไม่สมบูรณ์ของ Gödelนับตั้งแต่งานในช่วงแรกนี้ ระบบแคลคูลัสลำดับ หรือที่เรียกว่าระบบ Gentzen [ ^{4 ] [ 5 ] [ 6 ] [ 7 ] และแนวคิดทั่วไปที่เกี่ยวข้องกับระบบเหล่านี้ ได้ถูกนำไปประยุกต์ ใช้}อย่างกว้างขวางในสาขาทฤษฎีการพิสูจน์ ตรรกศาสตร์ทางคณิตศาสตร์ และ การ อนุมาน อัตโนมัติ

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

${\displaystyle B}$

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

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

ในการอนุมานเชิงธรรมชาติ การตัดสินใจมีรูปแบบดังนี้

${\displaystyle A_{1},A_{2},\ldots ,A_{n}\vdash B}$

โดยที่'s และ 's ก็คือสูตรและ 's อีกครั้งกล่าวอีกนัยหนึ่ง การตัดสินประกอบด้วยรายการ (อาจว่างเปล่า) ของสูตรทางด้านซ้ายมือของสัญลักษณ์ประตูหมุน " " โดยมีสูตรเดียวทางด้านขวามือ^{[ 8 ] [ 9 ] [ 10 ]} (แม้ว่าการเรียงสับเปลี่ยนของ's มักจะไม่สำคัญ) ทฤษฎีบทคือสูตรเหล่านั้นที่(โดยมีด้านซ้ายมือว่างเปล่า) เป็นข้อสรุปของการพิสูจน์ที่ถูกต้อง (ในการนำเสนอการอนุมานตามธรรมชาติบางอย่างs และประตูหมุนไม่ได้เขียนลงอย่างชัดเจน แต่จะใช้สัญกรณ์สองมิติที่สามารถอนุมานได้แทน) ${\displaystyle A_{i}}$${\displaystyle B}$${\displaystyle n\geq 0}$${\displaystyle \vdash }$${\displaystyle A_{i}}$${\displaystyle B}$${\displaystyle \vdash B}$${\displaystyle A_{i}}$

ความหมายมาตรฐานของการตัดสินในการอนุมานตามธรรมชาติคือการยืนยันว่าเมื่อใดก็ตามที่^{[ 11 ]} , , เป็นต้น เป็นจริงทั้งหมดก็จะเป็นจริงด้วย การตัดสิน ${\displaystyle A_{1}}$${\displaystyle A_{2}}$${\displaystyle B}$

${\displaystyle A_{1},\ldots ,A_{n}\vdash B}$

และ

${\displaystyle \vdash (A_{1}\land \cdots \land A_{n})\rightarrow B}$

ทั้งสองอย่างเทียบเท่ากันในความหมายที่เข้มงวด กล่าวคือ การพิสูจน์ข้อใดข้อหนึ่งสามารถขยายไปสู่การพิสูจน์อีกข้อหนึ่งได้

สุดท้ายนี้ แคลคูลัสลำดับจะขยายรูปแบบของการตัดสินโดยการอนุมานตามธรรมชาติไปสู่

${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},}$

วัตถุทางไวยากรณ์ที่เรียกว่าลำดับ สูตรทางด้านซ้ายของช่องหมุนเรียกว่าส่วนนำและสูตรทางด้านขวาเรียกว่าส่วนตามหรือผลที่ตามมารวมกันเรียกว่าสูตรลำดับหรือสูตรลำดับ^{[ 12 ]}อีกครั้งและเป็นสูตร และและเป็นจำนวนเต็มที่ไม่เป็นลบ นั่นคือ ด้านซ้ายหรือด้านขวา (หรือทั้งสองด้าน) อาจว่างเปล่า เช่นเดียวกับการอนุมานตามธรรมชาติ ทฤษฎีบทคือทฤษฎีบทที่เป็นข้อสรุปของการพิสูจน์ที่ถูกต้อง ${\displaystyle A_{i}}$${\displaystyle B_{i}}$${\displaystyle n}$${\displaystyle k}$${\displaystyle B}$${\displaystyle \vdash B}$

ความหมายมาตรฐานของลำดับคือการยืนยันว่าเมื่อใดก็ตามที่ทุกอย่าง เป็นจริงอย่างน้อยหนึ่งอย่างก็จะเป็นจริงด้วย^{[ 13 ]}ดังนั้นลำดับที่ว่างเปล่าซึ่งมีตัวดำเนินการทั้งสองว่างเปล่าจึงเป็นเท็จ^{[ 14 ]}วิธีหนึ่งในการแสดงสิ่งนี้คือควรคิดว่าเครื่องหมายจุลภาคทางซ้ายของประตูหมุนเป็น "และ" และเครื่องหมายจุลภาคทางขวาของประตูหมุนเป็น "หรือ" (รวมอยู่ด้วย) ลำดับ ${\displaystyle A_{i}}$${\displaystyle B_{i}}$

${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k}}$

และ

${\displaystyle \vdash (A_{1}\land \cdots \land A_{n})\rightarrow (B_{1}\lor \cdots \lor B_{k})}$

มีความเทียบเท่ากันในความหมายที่เข้มงวด กล่าวคือ การพิสูจน์ลำดับหนึ่งสามารถขยายไปสู่การพิสูจน์ลำดับอีกอันได้

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

${\displaystyle \vdash \neg A_{1}\lor \neg A_{2}\lor \cdots \lor \neg A_{n}\lor B_{1}\lor B_{2}\lor \cdots \lor B_{k}}$

(อย่างน้อยหนึ่งในข้อ A เป็นเท็จ หรือหนึ่งในข้อ B เป็นจริง)

หรือเช่น

${\displaystyle \vdash \neg (A_{1}\land A_{2}\land \cdots \land A_{n}\land \neg B_{1}\land \neg B_{2}\land \cdots \land \neg B_{k})}$

(เป็นไปไม่ได้ที่ข้อ A ทั้งหมดจะเป็นจริงและข้อ B ทั้งหมดจะเป็นเท็จ)

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

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

Gentzen ยืนยันความแตกต่างที่ชัดเจนระหว่างระบบการอนุมานเชิงธรรมชาติแบบเอาต์พุตเดียว (NK และ NJ) และระบบแคลคูลัสลำดับแบบเอาต์พุตหลายตัว (LK และ LJ) เขาเขียนว่าระบบการอนุมานเชิงธรรมชาติแบบสัญชาตญาณ NJ นั้นค่อนข้างน่าเกลียด^{[ 17 ]}เขากล่าวว่าบทบาทพิเศษของตัวกลางที่ถูกยกเว้นในระบบการอนุมานเชิงธรรมชาติแบบคลาสสิก NK นั้นถูกลบออกไปในระบบแคลคูลัสลำดับแบบคลาสสิก LK ^{[ 18 ]}เขากล่าวว่าแคลคูลัสลำดับ LJ ให้ความสมมาตรมากกว่าการอนุมานเชิงธรรมชาติ NJ ในกรณีของตรรกะแบบสัญชาตญาณ เช่นเดียวกับในกรณีของตรรกะแบบคลาสสิก (LK เทียบกับ NK) ^{[ 19 ]}จากนั้นเขากล่าวว่านอกเหนือจากเหตุผลเหล่านี้แล้ว แคลคูลัสลำดับที่มีสูตรสืบทอดหลายสูตรนั้นมีจุดประสงค์โดยเฉพาะสำหรับทฤษฎีบทหลักของเขา ("Hauptsatz") ^{[ 20 ]}

คำว่า "sequent" มาจากคำว่า "Sequenz" ในบทความของ Gentzen ในปี 1934 ^{[ 1 ]} Kleeneแสดงความคิดเห็นเกี่ยวกับการแปลเป็นภาษาอังกฤษดังนี้: "Gentzen กล่าวว่า 'Sequenz' ซึ่งเราแปลว่า 'sequent' เพราะเราใช้คำว่า 'sequence' ไปแล้วสำหรับลำดับของวัตถุใดๆ โดยที่ในภาษาเยอรมันคือ 'Folge'" ^{[ 21 ]}

Gentzen ใช้ตัวพิมพ์ใหญ่สองตัวเพื่อแทนระบบการพิสูจน์ต่างๆ ในบทความปี 1935 ของเขา เขาระบุว่าในLK นั้นLหมายถึง "logische" (ตรรกะ) และKหมายถึง "klassische Pradikatenlogik" ("ตรรกะเชิงทำนายแบบคลาสสิก") ส่วนJในLJหมายถึง "intuitionistische Pradikatenlogik" ("ตรรกะเชิงทำนายแบบสัญชาตญาณ") ^{[ 1 ] : 177} ในทำนองเดียวกันNในNKและNJหมายถึง "natürlichen Schließens" ("การอนุมานตามธรรมชาติ") ไม่ชัดเจนว่าเขาใช้Jแทน "intuitionistische" ได้อย่างไร แต่สันนิษฐานว่าเพื่อแยกความแตกต่างทางด้านการพิมพ์จากเลข 1 และเลขโรมัน I ในที่อื่นๆ Gentzen ใช้LIและNIแทนLJและNJ ^{[ 22 ] :} 83

แคลคูลัสลำดับสามารถมองได้ว่าเป็นเครื่องมือสำหรับการพิสูจน์สูตรในตรรกะเชิงประพจน์คล้ายกับวิธีการของตารางวิเคราะห์ โดยให้ขั้นตอนต่างๆ ที่ช่วยให้สามารถลดปัญหาการพิสูจน์สูตรตรรกะให้เหลือสูตรที่ง่ายขึ้นเรื่อยๆ จนกระทั่งได้สูตรที่ไม่สำคัญ^{[ 23 ]}

พิจารณาสูตรต่อไปนี้:

${\displaystyle ((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)}$

ข้อความนี้เขียนในรูปแบบต่อไปนี้ โดยข้อเสนอที่ต้องพิสูจน์จะอยู่ทางด้านขวาของสัญลักษณ์ประตูหมุน : ${\displaystyle \vdash }$

${\displaystyle \vdash ((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)}$

ตอนนี้ แทนที่จะพิสูจน์สิ่งนี้จากสัจพจน์ ก็เพียงพอที่จะสมมติข้อตั้งต้นของการบ่งชี้แล้วลองพิสูจน์ข้อสรุปของมัน^{[ 24 ]}ดังนั้นจึงเคลื่อนไปยังลำดับต่อไปนี้:

${\displaystyle (p\rightarrow r)\lor (q\rightarrow r)\vdash (p\land q)\rightarrow r}$

อีกครั้งที่ด้านขวามือประกอบด้วยนัยยะแฝง ซึ่งสามารถสันนิษฐานข้อตั้งต้นได้อีก ดังนั้นจึงจำเป็นต้องพิสูจน์เพียงข้อสรุปเท่านั้น:

${\displaystyle (p\rightarrow r)\lor (q\rightarrow r),(p\land q)\vdash r}$

เนื่องจากถือว่าตัวแปรทางด้านซ้ายมือมีความสัมพันธ์กันโดยการเชื่อมโยงจึงสามารถแทนที่ด้วยสิ่งต่อไปนี้ได้:

${\displaystyle (p\rightarrow r)\lor (q\rightarrow r),p,q\vdash r}$

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

${\displaystyle p\rightarrow r,p,q\vdash r}$

${\displaystyle q\rightarrow r,p,q\vdash r}$

ในกรณีของการตัดสินครั้งแรก เราเขียนใหม่เป็นและแยกซีเควนซ์อีกครั้งเพื่อให้ได้: ${\displaystyle p\rightarrow r}$${\displaystyle \lnot p\lor r}$

${\displaystyle \lnot p,p,q\vdash r}$

${\displaystyle r,p,q\vdash r}$

ลำดับที่สองเสร็จสมบูรณ์แล้ว ลำดับแรกสามารถลดรูปให้ง่ายขึ้นได้อีกดังนี้:

${\displaystyle p,q\vdash p,r}$

กระบวนการนี้สามารถดำเนินต่อไปได้เรื่อยๆ จนกว่าจะเหลือเพียงสูตรอะตอมในแต่ละด้าน กระบวนการนี้สามารถอธิบายได้ด้วยภาพต้นไม้ที่มีรากดังแสดงในภาพด้านขวา รากของต้นไม้คือสูตรที่เราต้องการพิสูจน์ ใบประกอบด้วยสูตรอะตอมเท่านั้น ต้นไม้นี้เรียกว่าต้นไม้ลดรูป^{[ 23 ] [ 25 ]}

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

ต่อไปนี้เป็นกฎที่ใช้ในการดำเนินการตามต้นไม้ เมื่อใดก็ตามที่ลำดับหนึ่งถูกแยกออกเป็นสองส่วน จุดยอดของต้นไม้จะมีจุดยอดลูกสองจุด และต้นไม้จะแตกกิ่งก้านสาขา นอกจากนี้ ยังสามารถเปลี่ยนแปลงลำดับของอาร์กิวเมนต์ในแต่ละด้านได้อย่างอิสระ โดย Γ และ Δ แทนอาร์กิวเมนต์เพิ่มเติมที่เป็นไปได้^{[ 23 ]}

โดยทั่วไปแล้ว เส้นแนวนอนที่ใช้ในรูปแบบการจัดวางแบบ Gentzen สำหรับการอนุมานตามธรรมชาติเรียกว่าเส้นอนุมาน^{[ 26 ]}

ซ้าย	ขวา
${\displaystyle L\land {\text{rule: }}\quad {\cfrac {\Gamma ,A\land B\vdash \Delta }{\Gamma ,A,B\vdash \Delta }}}$	${\displaystyle R\land {\text{rule: }}{\cfrac {\Gamma \vdash \Delta ,A\land B}{\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}}}$
${\displaystyle L\lor {\text{rule: }}{\cfrac {\Gamma ,A\lor B\vdash \Delta }{\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }}}$	${\displaystyle R\lor {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,A\lor B}{\Gamma \vdash \Delta ,A,B}}}$
${\displaystyle L\rightarrow {\text{rule: }}{\cfrac {\Gamma ,A\rightarrow B\vdash \Delta }{\Gamma \vdash \Delta ,A\qquad \Gamma ,B\vdash \Delta }}}$	${\displaystyle R\rightarrow {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,A\rightarrow B}{\Gamma ,A\vdash \Delta ,B}}}$
${\displaystyle L\lnot {\text{rule: }}\quad {\cfrac {\Gamma ,\lnot A\vdash \Delta }{\Gamma \vdash \Delta ,A}}}$	${\displaystyle R\lnot {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,\lnot A}{\Gamma ,A\vdash \Delta }}}$
สัจพจน์: ${\displaystyle \Gamma ,A\vdash \Delta ,A}$

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

ดังนั้น ลำดับในใบของต้นไม้จึงประกอบด้วยสัญลักษณ์อะตอมเท่านั้น ซึ่งอาจพิสูจน์ได้ด้วยสัจพจน์หรือไม่ก็ได้ ขึ้นอยู่กับว่าสัญลักษณ์ใดสัญลักษณ์หนึ่งทางด้านขวาปรากฏอยู่ทางด้านซ้ายด้วยหรือไม่

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

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

ส่วนนี้แนะนำกฎของแคลคูลัสลำดับLK (ย่อมาจาก Logistische Kalkül) ตามที่ Gentzen แนะนำในปี พ.ศ. 2477 ^{[ 27 ]}การพิสูจน์ (อย่างเป็นทางการ) ในแคลคูลัสนี้คือลำดับ จำกัด ของลำดับ โดยที่ลำดับแต่ละลำดับสามารถอนุมานได้จากลำดับที่ปรากฏก่อนหน้าในลำดับโดยใช้กฎข้อ ใดข้อหนึ่ง ด้านล่าง

จะใช้สัญลักษณ์ดังต่อไปนี้:

• ${\displaystyle \vdash }$สิ่งที่เรียกว่า " ประตูหมุน"นั้น จะแยกสมมติฐานทางด้านซ้ายออกจากข้อเสนอทางด้านขวา
• ${\displaystyle A}$และใช้เพื่อแสดงถึงสูตรของ ตรรกศาสตร์ ภาคแสดงลำดับที่หนึ่ง (อาจจำกัดเฉพาะตรรกศาสตร์เชิงประพจน์ก็ได้)${\displaystyle B}$
• ${\displaystyle \Gamma ,\Delta ,\Sigma }$และเป็นลำดับของสูตรที่มีจำนวนจำกัด (อาจว่างเปล่า) (อันที่จริง ลำดับของสูตรไม่สำคัญ ดู§ กฎโครงสร้าง ) เรียกว่า บริบท ${\displaystyle \Pi }$
  • เมื่ออยู่ทางด้านซ้ายของเครื่องหมายจุลภาค ลำดับของสูตรจะถูกพิจารณาแบบเชื่อมโยงกัน (โดยถือว่าทุกสูตรเป็นจริงพร้อมกัน)${\displaystyle \vdash }$
  • ในขณะที่ทางด้านขวาของเครื่องหมายจุลภาค ลำดับของสูตรจะถูกพิจารณาแบบแยกส่วน (อย่างน้อยหนึ่งสูตรจะต้องเป็นจริงสำหรับการกำหนดค่าตัวแปรใดๆ)${\displaystyle \vdash }$
• ${\displaystyle t}$หมายถึงคำศัพท์ที่กำหนดขึ้นโดยพลการ
• ${\displaystyle x}$และใช้เพื่อระบุตัวแปร${\displaystyle y}$
• ตัวแปรจะเรียกว่าเป็นอิสระภายในสูตร หากไม่ได้ถูกผูกมัดด้วยตัวบ่งปริมาณหรือ ตัว กำหนด ปริมาณ${\displaystyle \forall }$${\displaystyle \exists }$
• ${\displaystyle A[t/x]}$หมายถึงสูตรที่ได้จากการแทนที่พจน์สำหรับทุกๆ การปรากฏอิสระของตัวแปรในสูตรโดยมีข้อจำกัดว่าพจน์นั้นต้องเป็นอิสระสำหรับตัวแปรใน(กล่าวคือ การปรากฏของตัวแปรใดๆ ใน จะไม่ถูกผูกมัดใน)${\displaystyle t}$${\displaystyle x}$${\displaystyle A}$${\displaystyle t}$${\displaystyle x}$${\displaystyle A}$${\displaystyle t}$${\displaystyle A[t/x]}$
• ${\displaystyle WL}$, , , , , : ตัวเลขทั้งหกนี้แทนกฎโครงสร้างสองเวอร์ชันของแต่ละกฎสามข้อ โดยเวอร์ชันหนึ่งใช้ทางด้านซ้าย ('L') ของและอีกเวอร์ชันหนึ่งใช้ทางด้านขวา ('R') กฎเหล่านี้ย่อว่า 'W' สำหรับการลดทอน (ซ้าย/ขวา) 'C' สำหรับการหดตัวและ 'P' สำหรับการเรียงสับเปลี่ยน${\displaystyle WR}$${\displaystyle CL}$${\displaystyle CR}$${\displaystyle PL}$${\displaystyle PR}$${\displaystyle \vdash }$

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

ในตารางด้านล่างหมายถึงส่วน เติมเต็มสัมพัทธ์ของใน${\displaystyle A\setminus B}$${\displaystyle B}$${\displaystyle A}$

สัจพจน์	ตัด
${\displaystyle {\cfrac {\qquad }{A\vdash A}}\quad (I)}$	${\displaystyle {\cfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})}$

กฎตรรกะด้านซ้าย	กฎตรรกะที่ถูกต้อง
${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})}$	${\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})}$
${\displaystyle {\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})}$	${\displaystyle {\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})}$
${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }{\Gamma ,A\lor B\vdash \Delta }}\quad ({\lor }L)}$	${\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Gamma \vdash B,\Delta }{\Gamma \vdash A\land B,\Delta }}\quad ({\land }R)}$
${\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)}$	${\displaystyle {\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)}$
${\displaystyle {\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma ,A\setminus B\vdash \Delta }}\quad ({\setminus }L)}$	${\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma \vdash A\setminus B,\Delta ,\Pi }}\quad ({\setminus }R)}$
${\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)}$	${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)}$
${\displaystyle {\cfrac {\Gamma ,A[t/x]\vdash \Delta }{\Gamma ,\forall xA\vdash \Delta }}\quad ({\forall }L)}$	${\displaystyle {\cfrac {\Gamma \vdash A[y/x],\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)}$(†)
${\displaystyle {\cfrac {\Gamma ,A[y/x]\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)}$(†)	${\displaystyle {\cfrac {\Gamma \vdash A[t/x],\Delta }{\Gamma \vdash \exists xA,\Delta }}\quad ({\exists }R)}$

กฎโครงสร้างด้านซ้าย	กฎโครงสร้างที่ถูกต้อง
${\displaystyle {\cfrac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {WL}})}$	${\displaystyle {\cfrac {\Gamma \vdash \Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {WR}})}$
${\displaystyle {\cfrac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {CL}})}$	${\displaystyle {\cfrac {\Gamma \vdash A,A,\Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {CR}})}$
${\displaystyle {\cfrac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}\quad ({\mathit {PL}})}$	${\displaystyle {\cfrac {\Gamma \vdash \Delta _{1},A,B,\Delta _{2}}{\Gamma \vdash \Delta _{1},B,A,\Delta _{2}}}\quad ({\mathit {PR}})}$

ข้อจำกัด : ในกฎที่ทำเครื่องหมาย (†) และตัวแปรต้องไม่ปรากฏแบบอิสระที่ใดในลำดับล่างที่เกี่ยวข้อง${\displaystyle ({\forall }R)}$${\displaystyle ({\exists }L)}$${\displaystyle y}$

กฎข้างต้นสามารถแบ่งออกเป็นสองกลุ่มหลัก ได้แก่ กฎเชิงตรรกะและ กฎ เชิงโครงสร้างกฎเชิงตรรกะแต่ละข้อจะนำเสนอสูตรตรรกะใหม่ทางด้านซ้ายหรือด้านขวาของช่องหมุน ในทางตรงกันข้าม กฎเชิงโครงสร้างจะทำงานกับโครงสร้างของลำดับ โดยไม่สนใจรูปร่างที่แน่นอนของสูตร ข้อยกเว้นสองประการสำหรับแผนการทั่วไปนี้คือ สัจพจน์เอกลักษณ์ (I) และกฎของ (Cut) ${\displaystyle \vdash }$

แม้ว่ากฎข้างต้นจะระบุไว้อย่างเป็นทางการ แต่ก็สามารถตีความได้อย่างเข้าใจง่ายในแง่ของตรรกศาสตร์คลาสสิก ตัวอย่างเช่น พิจารณากฎข้อที่ 1 กฎนี้กล่าวว่า เมื่อใดก็ตามที่สามารถพิสูจน์ได้ว่าสามารถสรุปได้จากลำดับของสูตรบางสูตรที่มีแล้ว ก็สามารถสรุปได้จากสมมติฐาน (ที่แข็งแกร่งกว่า) ว่าเป็นจริงเช่นกัน ในทำนองเดียวกัน กฎข้อที่ 2 กล่าวว่า ถ้าและเพียงพอที่จะสรุปได้ว่า แล้วจากเพียงอย่างเดียวก็ยังสามารถสรุปได้ว่าหรือว่าต้องเป็นเท็จ กล่าวคือเป็นจริง กฎทั้งหมดสามารถตีความได้ในลักษณะนี้ ${\displaystyle ({\land }L_{1})}$${\displaystyle \Delta }$${\displaystyle A}$${\displaystyle \Delta }$${\displaystyle A\land B}$${\displaystyle ({\neg }R)}$${\displaystyle \Gamma }$${\displaystyle A}$${\displaystyle \Delta }$${\displaystyle \Gamma }$${\displaystyle \Delta }$${\displaystyle A}$${\displaystyle {\neg }A}$

เพื่อให้เข้าใจกฎของตัวบ่งปริมาณได้ง่ายขึ้น ลองพิจารณากฎข้อนี้ดู แน่นอนว่าโดยทั่วไปแล้ว การสรุปว่าเป็นจริงเพียงเพราะเป็นจริงนั้นเป็นไปไม่ได้ อย่างไรก็ตาม หากตัวแปรyไม่ได้ถูกกล่าวถึงที่อื่น (กล่าวคือ ยังสามารถเลือกได้อย่างอิสระโดยไม่ส่งผลต่อสูตรอื่นๆ) ก็สามารถสันนิษฐานได้ว่าเป็นจริงสำหรับค่าใดๆ ของyจากนั้นกฎอื่นๆ ก็จะค่อนข้างตรงไปตรงมา ${\displaystyle ({\forall }R)}$${\displaystyle \forall {x}A}$${\displaystyle A[y/x]}$${\displaystyle A[y/x]}$

แทนที่จะมองกฎเป็นคำอธิบายสำหรับการอนุมานทางกฎหมายในตรรกศาสตร์ภาคแสดง เราอาจมองว่ากฎเหล่านั้นเป็นคำแนะนำสำหรับการสร้างบทพิสูจน์สำหรับข้อความที่กำหนด ในกรณีนี้ กฎสามารถอ่านจากล่างขึ้นบนได้ ตัวอย่างเช่นกล่าวว่า เพื่อพิสูจน์ว่าเป็นผลมาจากสมมติฐานและก็เพียงพอที่จะพิสูจน์ว่าสามารถสรุปได้จากและสามารถสรุปได้จากตามลำดับ โปรดทราบว่า เมื่อกำหนดเงื่อนไขเบื้องต้นแล้ว ยังไม่ชัดเจนว่าจะแยกเงื่อนไขนี้ออกเป็นและ ได้อย่างไร อย่างไรก็ตาม มีความเป็นไปได้เพียงจำนวนจำกัดเท่านั้นที่จะตรวจสอบได้ เนื่องจากเงื่อนไขเบื้องต้นตามสมมติฐานมีจำนวนจำกัด นี่แสดงให้เห็นว่าทฤษฎีการพิสูจน์สามารถมองได้ว่าทำงานกับบทพิสูจน์ในลักษณะเชิงการจัดเรียง กล่าวคือ เมื่อกำหนดบทพิสูจน์สำหรับทั้งและแล้ว เราสามารถสร้างบทพิสูจน์สำหรับได้ ${\displaystyle ({\land }R)}$${\displaystyle A\land B}$${\displaystyle \Gamma }$${\displaystyle \Sigma }$${\displaystyle A}$${\displaystyle \Gamma }$${\displaystyle B}$${\displaystyle \Sigma }$${\displaystyle \Gamma }$${\displaystyle \Sigma }$${\displaystyle A}$${\displaystyle B}$${\displaystyle A\land B}$

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

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

สังเกตว่า หากเราละเว้นตัวเชื่อมที่ไม่เป็นมาตรฐาน \ กฎทั้งหมดจะมีคู่สมมาตร ยกเว้นกฎสำหรับการบ่งชี้ นี่สะท้อนให้เห็นว่าภาษาปกติของตรรกศาสตร์ลำดับที่หนึ่งไม่ได้รวมตัวเชื่อม "ไม่ได้ถูกบ่งชี้โดย" ซึ่งจะเป็นคู่ตรงข้ามของเดอ มอร์แกนของการบ่งชี้ การเพิ่มตัวเชื่อมดังกล่าวพร้อมกฎตามธรรมชาติจะทำให้แคลคูลัสมีความสมมาตรซ้ายขวาอย่างสมบูรณ์ ${\displaystyle \not \leftarrow }$

นี่คือที่มาของ " " ซึ่งรู้จักกันในชื่อกฎแห่งการยกเว้นตรงกลาง ( tertium non daturในภาษาละติน) ${\displaystyle \vdash A\lor \lnot A}$

		${\displaystyle (I)}$
${\displaystyle A\vdash A}$
		${\displaystyle (\lnot R)}$
${\displaystyle \vdash \lnot A,A}$
		${\displaystyle (\lor R_{2})}$
${\displaystyle \vdash A\lor \lnot A,A}$
		${\displaystyle (PR)}$
${\displaystyle \vdash A,A\lor \lnot A}$
		${\displaystyle (\lor R_{1})}$
${\displaystyle \vdash A\lor \lnot A,A\lor \lnot A}$
		${\displaystyle (CR)}$
${\displaystyle \vdash A\lor \lnot A}$

ต่อไปคือการพิสูจน์ข้อเท็จจริงง่ายๆ ที่เกี่ยวข้องกับตัวบ่งปริมาณ โปรดทราบว่าข้อความกลับกันนั้นไม่เป็นจริง และสามารถเห็นความเท็จได้เมื่อพยายามพิสูจน์จากล่างขึ้นบน เนื่องจากตัวแปรอิสระที่มีอยู่ไม่สามารถนำมาใช้แทนที่ในกฎและได้ ${\displaystyle (\forall R)}$${\displaystyle (\exists L)}$

		${\displaystyle (I)}$
${\displaystyle p(x,y)\vdash p(x,y)}$
		${\displaystyle (\forall L)}$
${\displaystyle \forall x\left(p(x,y)\right)\vdash p(x,y)}$
		${\displaystyle (\exists R)}$
${\displaystyle \forall x\left(p(x,y)\right)\vdash \exists y\left(p(x,y)\right)}$
		${\displaystyle (\exists L)}$
${\displaystyle \exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \exists y\left(p(x,y)\right)}$
		${\displaystyle (\forall R)}$
${\displaystyle \exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \forall x\left(\exists y\left(p(x,y)\right)\right)}$

เพื่อสิ่งที่น่าสนใจยิ่งกว่า เราจะพิสูจน์สิ่งนี้การหาที่มาของข้อพิสูจน์นั้นทำได้ง่าย ซึ่งแสดงให้เห็นถึงประโยชน์ของ LK ในการพิสูจน์อัตโนมัติ ${\displaystyle {\left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}}$

${\displaystyle (I)}$ ${\displaystyle A\vdash A}$     ${\displaystyle (\lnot R)}$ ${\displaystyle \vdash \lnot A,A}$     ${\displaystyle (PR)}$ ${\displaystyle \vdash A,\lnot A}$            ${\displaystyle (I)}$ ${\displaystyle B\vdash B}$     ${\displaystyle (WR)}$ ${\displaystyle B\vdash B,C}$            ${\displaystyle (I)}$ ${\displaystyle C\vdash C}$     ${\displaystyle (WR)}$ ${\displaystyle C\vdash B,C}$         ${\displaystyle (\lor L)}$ ${\displaystyle B\lor C\vdash B,C}$     ${\displaystyle (PR)}$ ${\displaystyle B\lor C\vdash C,B}$     ${\displaystyle (\lnot L)}$ ${\displaystyle B\lor C,\lnot C\vdash B}$              ${\displaystyle (I)}$ ${\displaystyle \lnot A\vdash \lnot A}$         ${\displaystyle (\rightarrow L)}$ ${\displaystyle \left(B\lor C\right),\lnot C,\left(B\rightarrow \lnot A\right)\vdash \lnot A}$     ${\displaystyle (\land L_{1})}$ ${\displaystyle \left(B\lor C\right),\lnot C,\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$     ${\displaystyle (PL)}$ ${\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\lnot C\vdash \lnot A}$     ${\displaystyle (\land L_{2})}$ ${\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$     ${\displaystyle (CL)}$ ${\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$     ${\displaystyle (PL)}$ ${\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(B\lor C\right)\vdash \lnot A}$		${\displaystyle (\rightarrow L)}$
${\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A,\lnot A}$
		${\displaystyle (CR)}$
${\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A}$
		${\displaystyle (PL)}$
${\displaystyle \left(A\rightarrow \left(B\lor C\right)\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$
		${\displaystyle (\rightarrow R)}$
${\displaystyle \left(A\rightarrow \left(B\lor C\right)\right)\vdash \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)}$
		${\displaystyle (\rightarrow R)}$
${\displaystyle \vdash \left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}$

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

สำหรับสูตรบางอย่าง (เช่น รูปแบบต่างๆ) ของแคลคูลัสลำดับ การพิสูจน์ในแคลคูลัสดังกล่าวจะสอดคล้องกับตารางวิเคราะห์ แบบปิดที่กลับ หัว^{[ 28 ]}

กฎเกณฑ์เชิงโครงสร้างนั้นสมควรได้รับการอธิบายเพิ่มเติมอีกเล็กน้อย

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

การหดตัว (C) และการเรียงสับเปลี่ยน (P) รับประกันว่าทั้งลำดับ (P) และจำนวนครั้งของการปรากฏ (C) ขององค์ประกอบในลำดับนั้นไม่มีผล ดังนั้น เราอาจพิจารณาเซต แทน ลำดับก็ได้

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

ระบบกฎนี้สามารถแสดงให้เห็นได้ว่าทั้งสมเหตุสมผลและสมบูรณ์เมื่อพิจารณาจากตรรกะลำดับแรก กล่าวคือ ข้อความจะตามมาทางความหมายจากชุดของข้อ สมมติ ก็ต่อเมื่อลำดับสามารถอนุมานได้โดยใช้กฎข้างต้น^{[ 29 ]}${\displaystyle A}$${\displaystyle \Gamma }$${\displaystyle (\Gamma \vDash A)}$${\displaystyle \Gamma \vdash A}$

ในแคลคูลัสลำดับ กฎของการตัดสามารถยอมรับได้ผลลัพธ์นี้ยังเรียกว่าทฤษฎีบทหลัก ของเกนท์เซน ("ทฤษฎีบทหลัก") ^{[ 2 ] [ 3 ]}

กฎข้างต้นสามารถปรับเปลี่ยนได้หลายวิธี:

มีอิสระในการเลือกบางส่วนเกี่ยวกับรายละเอียดทางเทคนิคของวิธีการกำหนดลำดับและกฎโครงสร้างอย่างเป็นทางการ โดยไม่เปลี่ยนแปลงลำดับที่ระบบสร้างขึ้น

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

กฎการลดทอนจะยอมรับได้หากมีการเปลี่ยนแปลงสัจพจน์ (I) เพื่อให้ได้ลำดับใดๆ ในรูปแบบการลดทอนใดๆ ที่ปรากฏในการพิสูจน์สามารถย้ายไปไว้ที่จุดเริ่มต้นของการพิสูจน์ได้ การเปลี่ยนแปลงนี้อาจสะดวกเมื่อสร้างการพิสูจน์จากล่างขึ้นบน ${\displaystyle \Gamma ,A\vdash A,\Delta }$

นอกจากนี้ ยังสามารถเปลี่ยนแปลงได้ว่ากฎที่มีข้อสมมติมากกว่าหนึ่งข้อจะใช้บริบทเดียวกันสำหรับแต่ละข้อสมมติเหล่านั้น หรือจะแบ่งบริบทระหว่างข้อสมมติเหล่านั้น ตัวอย่างเช่นอาจกำหนดกฎใหม่ได้ดังนี้ ${\displaystyle ({\lor }L)}$

${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}.}$

การหดตัวและการลดทอนทำให้กฎเวอร์ชันนี้สามารถอนุมานแทนกันได้กับเวอร์ชันข้างต้น แม้ว่าในกรณีที่ไม่มีการหดตัวและการลดทอน เช่นในตรรกะเชิงเส้นกฎเหล่านี้จะกำหนดตัวเชื่อมที่แตกต่างกัน

เราสามารถแนะนำค่าคงที่ความไร้สาระซึ่งแทนความเท็จได้โดยใช้สัจพจน์: ${\displaystyle \bot }$

${\displaystyle {\cfrac {}{\bot \vdash \quad }}}$

หรือหากการอ่อนค่าเป็นกฎที่ยอมรับได้ตามที่อธิบายไว้ข้างต้น ก็ให้เป็นไปตามสัจพจน์ดังนี้:

${\displaystyle {\cfrac {}{\Gamma ,\bot \vdash \Delta }}}$

ด้วยเหตุนี้การปฏิเสธจึงสามารถถูกรวมเข้าเป็นกรณีพิเศษของการบ่งชี้โดยนัยได้ ผ่านทางนิยาม ${\displaystyle \bot }$${\displaystyle (\neg A)\iff (A\to \bot )}$

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

ที่น่าประหลาดใจคือ การเปลี่ยนแปลงเล็กน้อยในกฎของ LK ก็เพียงพอที่จะเปลี่ยนให้เป็นระบบพิสูจน์สำหรับตรรกะเชิงสัญชาตญาณได้^{[ 30 ]}เพื่อจุดประสงค์นี้ เราต้องจำกัดลำดับที่มีสูตรทางด้านขวาไม่เกินหนึ่งสูตร^{[ 31 ]}และแก้ไขกฎเพื่อรักษาความไม่เปลี่ยนแปลงนี้ไว้ ตัวอย่างเช่นจะถูกกำหนดใหม่ดังนี้ (โดยที่ C เป็นสูตรใดๆ): ${\displaystyle ({\lor }L)}$

${\displaystyle {\cfrac {\Gamma ,A\vdash C\qquad \Gamma ,B\vdash C}{\Gamma ,A\lor B\vdash C}}\quad ({\lor }L)}$

ระบบที่ได้เรียกว่า LJ (Last Junction Logic) ระบบนี้มีความถูกต้องและสมบูรณ์ตามหลักตรรกศาสตร์เชิงสัญชาตญาณ และยอมรับการพิสูจน์แบบตัดทอนที่คล้ายคลึงกัน สามารถนำไปใช้ในการพิสูจน์คุณสมบัติการเชื่อมโยงแบบ "หรือ" และคุณสมบัติการมีอยู่ได้

อันที่จริง กฎเพียงข้อเดียวใน LK ที่จำเป็นต้องจำกัดให้ใช้กับผลลัพธ์แบบสูตรเดียวคือ( ซึ่งสามารถมองได้ว่าเป็นกรณีพิเศษของดังที่ได้อธิบายไว้ข้างต้น) และเมื่อตีความผลลัพธ์แบบหลายสูตรเป็นการเชื่อมแบบเลือก กฎการอนุมานอื่นๆ ทั้งหมดของ LK สามารถอนุมานได้ใน LJ ในขณะที่กฎและจะกลายเป็น ${\displaystyle ({\to }R)}$${\displaystyle (\neg R)}$${\displaystyle {\to }R}$${\displaystyle ({\forall }R)}$${\displaystyle ({\to }R)}$${\displaystyle ({\forall }R)}$

${\displaystyle {\cfrac {\Gamma ,A\vdash B\lor C}{\Gamma \vdash (A\to B)\lor C}}}$

และ (เมื่อไม่เกิดขึ้นอย่างอิสระในลำดับล่าง) ${\displaystyle y}$

${\displaystyle {\cfrac {\Gamma \vdash A[y/x]\lor C}{\Gamma \vdash (\forall xA)\lor C}}.}$

กฎสองข้อนี้ไม่ถูกต้องตามสัญชาตญาณ

• แคลคูลัสบ่อยครั้ง
• แคลคูลัสลำดับซ้อน
• ความละเอียด (ตรรกะ)
• ทฤษฎีการพิสูจน์

• ราธเจน, ไมเคิล; ซีก, วิลฟรีด (2024) "ทฤษฎีการพิสูจน์ (แคลคูลัสตามลำดับ)" . ในซัลตา, Edward N. ; โนเดลแมน, อูริ (บรรณาธิการ). สารานุกรมปรัชญาสแตนฟอร์ด (ฤดูหนาว 2024 เอ็ด)
• "แคลคูลัสลำดับ" , สารานุกรมคณิตศาสตร์ , EMS Press , 2001 [1994]
• "การเบี่ยงเบนสั้นๆ: แคลคูลัสลำดับ"คณิตศาสตร์ดี คณิตศาสตร์ไม่ดี 2 สิงหาคม 2553 สืบค้นเมื่อ 27 มีนาคม 2568
• "บทเรียนเชิงโต้ตอบเกี่ยวกับแคลคูลัสลำดับ" Logitext (MIT) สืบค้นเมื่อ 27 มีนาคม 2025