การอนุมานเชิงธรรมชาติและแคลคูลัสแบบซีเควนต์

การอนุมานเชิงธรรมชาติ (natural deduction) และแคลคูลัสแบบซีเควนต์ (sequent calculus) เป็นระบบรูปนัยแบบเกนท์เซน (Gentzen-style formal systems) สองระบบที่แสดงการพิสูจน์ผ่านกฎการนำเข้า (introduction rules) และกฎการกำจัด (elimination rules) สำหรับตัวเชื่อมตรรกะ ซึ่งเป็นกลไกพื้นฐานของทฤษฎีการพิสูจน์เชิงโครงสร้าง (structural proof theory)

Definition

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

Scope

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

Core questions

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

Key theories

กฎการนำเข้าและการกำจัด

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

ทฤษฎีบทการทำให้เป็นรูปแบบปกติ

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

ความสอดคล้องกันของแคลคูลัสทั้งสอง

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

Clinical relevance

แคลคูลัสเหล่านี้เป็นรูปแบบมาตรฐานสำหรับการศึกษาการพิสูจน์เชิงโครงสร้าง: การอนุมานเชิงธรรมชาติเป็นพื้นฐานของทฤษฎีประเภท (type theory) และผู้ช่วยการพิสูจน์ (proof assistants) ผ่านความสอดคล้องกันของการพิสูจน์ในฐานะโปรแกรม (proofs-as-programs correspondence) ในขณะที่แคลคูลัสแบบซีเควนต์ ซึ่งมีคุณสมบัติของสูตรย่อย (subformula property) หลังจากการกำจัดคัต (cut-elimination) เป็นพื้นฐานของการค้นหาการพิสูจน์อัตโนมัติ (automated proof search) และตารางวิเคราะห์ (analytic tableaux)

History

เกนท์เซนได้นำเสนอทั้งการอนุมานเชิงธรรมชาติและแคลคูลัสแบบซีเควนต์ในปี 1934 และ 1935 โดยได้คิดค้นแคลคูลัสแบบซีเควนต์เพื่อใช้ในการพิสูจน์ทฤษฎีบทการกำจัดคัต (cut-elimination theorem) ของเขา หลังจากพบว่าการอนุมานเชิงธรรมชาติวิเคราะห์ได้ยากกว่า พราวิตซ์ได้ฟื้นฟูการอนุมานเชิงธรรมชาติในปี 1965 ด้วยการศึกษาการทำให้เป็นรูปแบบปกติอย่างละเอียด และระบบเหล่านี้ได้กลายเป็นหัวใจสำคัญของการพัฒนาการพิสูจน์ในฐานะโปรแกรมในเวลาต่อมา

Key figures

• Gerhard Gentzen
• Dag Prawitz
• Stanislaw Jaskowski
• Jan von Plato

Seminal works

• troelstra2000
• prawitz1965
• negri2001

Frequently asked questions

ความแตกต่างระหว่างการอนุมานเชิงธรรมชาติและแคลคูลัสแบบซีเควนต์คืออะไร?

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

เหตุใดการทำให้เป็นรูปแบบปกติจึงมีความสำคัญ?

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