ความสอดคล้องของ New Foundations – บทพิสูจน์ทางคณิตศาสตร์อันซับซ้อนที่พิสูจน์ด้วย Lean

 (leanprover-community.github.io)
1 คะแนน โดย GN⁺ 2024-04-24 | 1 ความคิดเห็น | แชร์ทาง WhatsApp

Here is a summary of the key points from the given article, organized using Markdown:

การพิสูจน์ความไม่ขัดแย้งของทฤษฎีเซต New Foundations

  • Randall Holmes อ้างมาตั้งแต่หลังปี 2010 ว่าได้พิสูจน์ความไม่ขัดแย้งของทฤษฎีเซต "New Foundations (NF)" ที่ Quine เสนอไว้ในปี 1937
  • ที่เก็บนี้พิสูจน์ว่า NF ไม่มีความขัดแย้งจริง โดยตรวจสอบส่วนที่ยากของบทพิสูจน์ของ Holmes ด้วยตัวพิสูจน์ทฤษฎีเชิงโต้ตอบ Lean
  • ขณะนี้บทพิสูจน์เสร็จสมบูรณ์แล้ว และสามารถดูข้อความทฤษฎีบทได้ที่ ConNF/Model/Result.lean

เป้าหมาย

  • เป็นที่ทราบกันว่า NF ไม่มีความขัดแย้ง ก็ต่อเมื่อ Tangled Type Theory (TTT) ไม่มีความขัดแย้ง
  • พิสูจน์ว่า NF ไม่มีความขัดแย้งโดยการสร้างแบบจำลองของ TTT อย่างเป็นรูปแบบใน Lean
  • งานนี้อาศัยบทพิสูจน์หลายเวอร์ชันของ Holmes แต่มีการแก้ไขและเพิ่มเติมจำนวนมากเพื่อให้เข้ากับทฤษฎีชนิดของ Lean
  • โครงการนี้พึ่งพา mathlib ซึ่งเป็นไลบรารีคณิตศาสตร์ของชุมชนที่เขียนด้วย Lean ทำให้สามารถใช้ผลลัพธ์ที่คุ้นเคยเกี่ยวกับคาร์ดินัลหรือกรุปได้โดยไม่ต้องพิสูจน์ใหม่เอง
  • แม้ว่า kernel ที่เชื่อถือได้ของ Lean จะตรวจสอบนิยามและทฤษฎีบททั้งหมดใน mathlib และในโครงการนี้แล้ว แต่ Lean ไม่สามารถตรวจสอบได้ว่าคำอธิบายของนิยามและทฤษฎีบทตรงกับคำอธิบายภาษาอังกฤษที่ตั้งใจไว้หรือไม่ ดังนั้นเมื่อตีความข้อสรุปจากโค้ดของโครงการนี้จึงต้องระมัดระวังในการแปลความจากภาษาอังกฤษ

ทฤษฎีชนิดพันกัน (TTT)

  • TTT เป็นทฤษฎีเซตแบบหลายซอร์ตที่มีความสัมพันธ์ความเท่ากัน "=" และความสัมพันธ์การเป็นสมาชิก "∈"
  • ซอร์ตถูกทำดัชนีด้วยลำดับเชิงอนันต์จำกัด λ และสมาชิกของ λ ถูกเรียกว่าดัชนีชนิด
  • สูตร "x = y" ถูกนิยามอย่างถูกต้องเมื่อ x และ y มีชนิดเดียวกัน และสูตร "x ∈ y" ถูกนิยามอย่างถูกต้องเมื่อ x มีชนิดใดก็ได้ที่เล็กกว่า y
  • หนึ่งในสัจพจน์ของ TTT คือสัจพจน์เชิงภาวะภายนอกที่ระบุว่าเซตของชนิด α ถูกกำหนดอย่างเอกลักษณ์โดยสมาชิกของชนิด β ใด ๆ ที่มี β < α
  • ตัวอย่างเช่น หากเซตสองเซตของชนิด α ต่างกัน ก็จะต้องมีสมาชิกชนิด β ที่ต่างกันสำหรับทุก β < α ซึ่งทำให้การสร้างแบบจำลองของ TTT เป็นเรื่องยาก

กลยุทธ์

  • การสร้างแบบจำลองใช้กลยุทธ์คร่าว ๆ ดังนี้:

    • การสร้างชนิดพื้นฐาน

      • กำหนดให้ λ เป็นลำดับเชิงอนันต์จำกัด, κ > λ เป็นลำดับปกติ, และ μ > κ เป็นคาร์ดินัล strong limit ที่มี cofinality อย่างน้อย κ
      • เรียกเซตที่มีขนาดเล็กกว่า κ ว่าเล็ก
      • สร้างชนิดช่วยที่เรียกว่าชนิดพื้นฐานที่ระดับ -1 ซึ่งอยู่ต่ำกว่าทุกชนิดที่ท้ายที่สุดจะเป็นส่วนหนึ่งของแบบจำลอง
      • เรียกสมาชิกของชนิดนี้ว่าอะตอม (ไม่ใช่อะตอมในความหมายของ ZFU หรือ NFU) โดยมีอะตอมจำนวน μ ตัว และถูกแบ่งเป็น litter ขนาด κ

    • การสร้างแต่ละชนิด

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

    • การควบคุมขนาดของแต่ละชนิด

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

    • ปิดการอุปนัย

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

ความเห็นของ GN⁺

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

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 2024-04-24
ความคิดเห็นบน Hacker News
  • ความเสี่ยงที่บทพิสูจน์ที่ใช้ Lean จะผิดพลาดมีน้อยมาก อย่างไรก็ตาม ไม่ว่าจะมีบั๊กใน Lean หรือไม่ ก็ยังต้องอ่านข้อสรุปอย่างระมัดระวังและตรวจสอบว่าสิ่งที่พิสูจน์ได้ตรงกับที่อ้างจริงหรือไม่ ซึ่งเป็นปัญหาที่รู้จักกันดีทั้งในงานตรวจสอบซอฟต์แวร์และคณิตศาสตร์
  • กรณีนี้ดูเหมือนจะเป็นกรณีแรกที่ใช้ proof assistant เพื่อคลี่คลายสถานะของบทพิสูจน์ที่ยาก ก่อนหน้านี้เคยมีโครงการที่ตรวจสอบบทพิสูจน์เดิมซึ่งมีองค์ประกอบการคำนวณขนาดใหญ่ที่ประมวลผลด้วยซอฟต์แวร์ที่ไม่น่าเชื่อถือ แต่กรณีนี้เป็นครั้งแรกที่สถานะเชิงญาณวิทยาของผลลัพธ์ยังไม่แน่นอนในวงการคณิตศาสตร์
  • มีการตั้งข้อสงสัยเกี่ยวกับความแตกต่างพื้นฐานระหว่าง Coq กับ Lean และว่าทั้งคู่ทำงานอยู่บนตรรกะแบบเดียวกันหรือไม่ โดยในการอภิปรายที่เกี่ยวข้องมีการกล่าวถึงเนื้อหาที่เข้าใจได้ยาก
  • ผู้สนับสนุน Lean มักมีแนวโน้มจะยกจุดที่ว่า Lean เป็นวิธีพิสูจน์ที่เหนือกว่าหนักเกินไป Lean เป็นเพียงวิธีพิสูจน์ทางเลือก และในฐานะภาษาโปรแกรมและระบบ มันก็มีบั๊กของตัวเองและพึ่งพาสแตกของไลบรารีจำนวนมากที่ผู้อื่นเขียนไว้อย่างมาก
  • แทนที่จะพูดว่า Lean บอกว่าบทพิสูจน์นี้ดีกว่า คงจะถูกต้องและตรงไปตรงมามากกว่าถ้าจะบอกว่า บทพิสูจน์ที่เขียนขึ้นได้รับการตรวจสอบโดยนักคณิตศาสตร์มนุษย์ และจากนั้นถูกแปลงไปเป็น Lean ซึ่งก็ตรวจสอบผ่านเช่นกัน คำอธิบายที่ว่า Lean มอบการตรวจสอบเพียงหนึ่งเดียวอันสมบูรณ์แบบนั้นไม่แม่นยำ หรืออย่างน้อยก็ยังไม่เคยเห็นคำอธิบายที่พูดเช่นนั้น
  • มีการขอคำอธิบายคร่าว ๆ ว่า formalization ของทฤษฎีเซต "New Foundations" มีจุดพิเศษหรือจุดใหม่อย่างไรเมื่อเทียบกับ formalization อื่น ๆ ในรูปแบบที่นักศึกษาปริญญาตรีคณิตศาสตร์หรือผู้เชี่ยวชาญด้านวิศวกรรมอ่านเข้าใจได้
  • มีคนสงสัยว่าแนวทางนี้ท้ายที่สุดจะนำไปสู่การพิสูจน์แบบร่วมมือกันและการ 'แก้บั๊ก' จนทำให้คณิตศาสตร์กลายเป็นกระบวนการคล้ายโค้ดบน GitHub หรือไม่
  • มีคำถามว่า ตามทฤษฎีบทของเกอเดลที่กล่าวว่าระบบที่ทรงพลังเพียงพอทุกระบบไม่สามารถแสดงความสอดคล้องภายในของตัวเองได้ เรื่องนี้ควรเข้าใจอย่างไร
  • อยากติดตามโครงการ mathlib ต่อไปแต่ไม่มีเวลา จึงสงสัยว่ามีวิธีเข้าร่วมแบบมีส่วนร่วมน้อยมากได้หรือไม่