นักพัฒนาคนหนึ่งได้เริ่มโครงการที่ทะเยอทะยานในการทำให้ Principia Mathematica ของ Bertrand Russell เป็นทางการโดยใช้ตัวพิสูจน์ทฤษฎี Lean4 ซึ่งจุดประกายให้เกิดการอภิปรายเกี่ยวกับความท้าทายทางปรัชญาและการปฏิบัติที่มีอยู่ในการดำเนินการดังกล่าว
โครงการนี้มีเป้าหมายที่จะแปลงการพิสูจน์ทางตรรกะที่ซับซ้อนของ Russell ให้เข้ากับกรอบการคำนวณสมัยใหม่ โดยนักพัฒนาได้ระบุว่าพวกเขากำลังตั้งตารอที่จะทำให้การพิสูจน์ 1+1 ที่เป็นที่รู้จักกันดีเป็นทางการ ปัจจุบัน โครงการนี้ดูเหมือนจะอยู่ในช่วงเริ่มต้น โดยมีเพียงทฤษฎีบทเชิงข้อเสนอเบื้องต้นเท่านั้นที่เสร็จสมบูรณ์
 |
|---|
| หน้าจากตำราคณิตศาสตร์ที่แสดงทฤษฎีและการพิสูจน์ตรรกะอย่างเป็นทางการ คล้ายกับสิ่งที่กำลังถูกทำให้เป็นทางการจาก Principia Mathematica ของ Russell |
ข้อจำกัดทางปรัชญาของ Principia
การอภิปรายในชุมชนเผยให้เห็นถึงความตึงเครียดขั้นพื้นฐานที่อยู่ในใจกลางของโครงการนี้ แม้ว่าการใช้งานทางเทคนิคใน Lean4 จะน่าประทับใจ แต่ผู้แสดงความคิดเห็นหลายคนชี้ให้เห็นว่า Principia Mathematica เองถูกมองว่ามีข้อบกพร่องขั้นพื้นฐานโดยบางคน ผู้แสดงความคิดเห็นคนหนึ่งอ้างถึงการอธิบายของ Freeman Dyson ที่เรียกมันว่าเป็นความล้มเหลวอันยิ่งใหญ่ โดยอธิบายเพิ่มเติมว่าทฤษฎีความไม่สมบูรณ์ของ Gödel ได้บั่นทอนเป้าหมายพื้นฐานของ Principia อย่างมีประสิทธิภาพ
Principia ถูกเขียนขึ้นในยุคปรัชญาตรรกะนิยมที่ไร้เดียงสาของคณิตศาสตร์ ซึ่งไม่สามารถคาดการณ์ปัญหาการตัดสินใจขั้นพื้นฐานที่สำคัญในตรรกะ เช่น ทฤษฎีความไม่สมบูรณ์ของ Godel หรือปัญหาการหยุด (Halting Problem)
บริบททางประวัติศาสตร์นี้มีความสำคัญอย่างยิ่งต่อการทำความเข้าใจทั้งความสำคัญและข้อจำกัดของโครงการทำให้เป็นทางการ งานของ Russell และ Whitehead เกิดขึ้นก่อนความเข้าใจสมัยใหม่ของเราเกี่ยวกับข้อจำกัดที่มีอยู่ในระบบที่เป็นทางการ ทำให้การทำให้เป็นทางการอย่างสมบูรณ์มีปัญหาโดยธรรมชาติ
 |
|---|
| การนำเสนอภาพโครงสร้างของการพิสูจน์ทางตรรกศาสตร์ ที่แสดงให้เห็นถึงความซับซ้อนและความท้าทายทางปรัชญาที่เกี่ยวข้องกับ Principia Mathematica |
แนวทางปรัชญาที่แข่งขันกัน
ความคิดเห็นเน้นย้ำถึงวิธีที่ชุมชนคณิตศาสตร์แบ่งออกเป็นค่ายปรัชญาต่างๆ หลังจากความท้าทายต่อตรรกะนิยมเกิดขึ้น นักรูปนิยม (ตัวแทนของคณิตศาสตร์กระแสหลัก) ยอมรับข้อความที่ไม่สามารถตัดสินได้ แต่ยืนยันว่าความจริงทางคณิตศาสตร์มีอยู่อย่างอิสระจากความสามารถของเราในการพิสูจน์ ในทางตรงกันข้าม นักสร้างสรรค์นิยมเทียบเท่าความจริงทางคณิตศาสตร์กับความสามารถในการพิสูจน์ ปฏิเสธกฎของตรรกะที่สามของ Aristotle และสร้างคณิตศาสตร์บนพื้นฐานตรรกะทางเลือก
ความแตกต่างทางปรัชญาเหล่านี้ไม่ใช่เพียงแค่ทางวิชาการ—พวกมันส่งผลโดยตรงต่อวิธีที่คนอาจเข้าถึงการทำให้ Principia เป็นทางการ นักพัฒนาโครงการจะต้องเผชิญกับการตัดสินใจอย่างหลีกเลี่ยงไม่ได้เกี่ยวกับวิธีการจัดการกับข้อความที่ Gödel พิสูจน์แล้วว่าไม่สามารถตัดสินได้ภายในระบบเอง
แนวทางปรัชญาหลักในการวางรากฐานทางคณิตศาสตร์
- Logicism: พยายามสร้างคณิตศาสตร์ทั้งหมดจากตรรกะบริสุทธิ์ (แนวทางของ Russell)
- Formalism: ยอมรับข้อความที่พิสูจน์ไม่ได้ แต่ยืนยันว่าความจริงทางคณิตศาสตร์มีอยู่อย่างอิสระ
- Constructivism: มองว่าความจริงทางคณิตศาสตร์คือความสามารถในการพิสูจน์ ปฏิเสธกฎของตรรกะที่เรียกว่า law of excluded middle
สถานะโครงการ
- ความคืบหน้าปัจจุบัน: เพียงทฤษฎีบทเชิงประพจน์เบื้องต้นเท่านั้น
- เป้าหมาย: การทำให้เป็นทางการอย่างสมบูรณ์ของเล่มแรกของ Principia Mathematica
- เป้าหมายสำคัญ: การพิสูจน์ "1+1"
การใช้งานทางเทคนิคและเครื่องมือ
แม้จะมีความท้าทายทางปรัชญาเหล่านี้ แต่ด้านเทคนิคของโครงการแสดงให้เห็นถึงความน่าสนใจ นักพัฒนาได้ใช้กลยุทธ์แบบกำหนดเองใน Lean4 เพื่อจำลองสัญลักษณ์ของ Russell โดยเฉพาะอย่างยิ่งสำหรับการให้เหตุผลแบบ syllogistic ความใส่ใจในการรักษาความซื่อสัตย์ต่องานดั้งเดิมในขณะที่ใช้ประโยชน์จากความสามารถในการพิสูจน์ทฤษฎีสมัยใหม่แสดงให้เห็นถึงวิธีการที่ใส่ใจ
ผู้แสดงความคิดเห็นบางคนแนะนำเครื่องมือทางเลือกเช่น Naproche ที่อาจเหมาะสำหรับงานการทำให้เป็นทางการประเภทนี้ สิ่งนี้เน้นย้ำถึงระบบนิเวศที่เติบโตของเครื่องมือการตรวจสอบอย่างเป็นทางการและการพิสูจน์ทฤษฎีที่มีให้กับนักคณิตศาสตร์และนักวิทยาศาสตร์คอมพิวเตอร์สมัยใหม่
โครงการนี้ แม้จะยังอยู่ในช่วงเริ่มต้น แต่เป็นตัวแทนของจุดตัดที่น่าสนใจระหว่างคณิตศาสตร์เชิงประวัติศาสตร์ ปรัชญาของตรรกะ และวิธีการคำนวณสมัยใหม่ในการตรวจสอบอย่างเป็นทางการ ไม่ว่าในที่สุดจะประสบความสำเร็จในเป้าหมายที่ทะเยอทะยานหรือไม่ก็ตาม มันให้ข้อมูลเชิงลึกที่มีคุณค่าเกี่ยวกับทั้งพลังและข้อจำกัดของระบบที่เป็นทางการในคณิตศาสตร์
อ้างอิง: Formalizing Bertrand Russell's Principia Mathematica Using Lean4