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

• ส่วนที่ยากในการพิสูจน์ความสอดคล้องของทฤษฎีเซต New Foundations ซึ่ง Quine เสนอในปี 1937 ได้รับการตรวจสอบด้วย Lean แล้ว และทฤษฎีบทหลักถูกรวบรวมไว้ใน ConNF/Model/Result.lean
• แนวทางนี้ใช้ผลลัพธ์ที่ว่าความสอดคล้องของ New Foundations และ Tangled Type Theory(TTT) เทียบเท่ากัน โดยสร้างโมเดล TTT อย่างเป็นทางการภายใน Lean
• การสร้างโมเดล TTT มีความยากสูงขึ้นเพราะ extensionality ซึ่งกำหนดว่าเซตต้องถูกกำหนดได้อย่างเป็นเอกลักษณ์จากสมาชิกประเภทที่ต่ำกว่า
• การสร้างโมเดลใช้ base type, t-set, allowable permutations, support ขนาดเล็ก และ preferred extension และต้องใช้ freedom of action theorem เพื่อควบคุมขนาดของประเภทด้วย μ
• เคอร์เนลของ Lean ตรวจสอบพิสูจน์ที่ formalize แล้ว แต่ไม่รับประกันว่าประโยค formal ตรงกับความหมายภาษาอังกฤษที่ตั้งใจไว้ ดังนั้นการตีความผลลัพธ์ต้องตรวจทานการแปลความระหว่างกัน

---

การตรวจสอบความสอดคล้องของ New Foundations ที่ทำสำเร็จด้วย Lean

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

การรันโค้ดในเครื่อง

• การรันในเครื่องทำได้โดยติดตั้ง elan แล้ว clone repository จากนั้นรันคำสั่งต่อไปนี้ที่ root ของ repository

lake exe cache get

• หลังจากนั้นสามารถดูโค้ดได้ใน editor อย่าง Visual Studio Code และสามารถ compile โดยตรงจาก command line ด้วย lake build

ความเชื่อมโยงระหว่าง New Foundations กับ TTT

• เป็นที่ทราบว่า New Foundations สอดคล้องก็ต่อเมื่อ Tangled Type Theory(TTT) สอดคล้องเท่านั้น
  • ผลลัพธ์ที่เกี่ยวข้องอยู่ใน theorem 1 ของ Holmes
• โปรเจกต์นี้สร้างโมเดล TTT อย่างเป็นทางการใน Lean และจากสิ่งนี้จึงได้ข้อสรุปบนกระดาษถึงความสอดคล้องของ New Foundations หรือ Con(NF)
• งานนี้อาศัยเอกสารพิสูจน์หลายฉบับของ Holmes เป็นพื้นฐาน แต่ต้องมีการเปลี่ยนแปลงและเพิ่มเติมจำนวนมากเพื่อให้เข้ากับ type theory ของ Lean
  • untangled.pdf
  • retangled.pdf
  • newnfdoc.pdf
  • maybedetangled.pdf

ฐานของการตรวจสอบด้วย Lean และข้อควรระวังในการตีความ

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

โครงสร้างและความยากของ Tangled Type Theory

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

ขั้นตอนหลักในการสร้างโมเดล

• การสร้าง base type

  • ให้ λ เป็น ordinal ลิมิต, κ > λ เป็น regular ordinal และ μ > κ เป็น strong limit cardinal ที่มี cofinality อย่างน้อย κ
  • เซตที่มีขนาดเล็กกว่า κ เรียกว่า small
  • เริ่มจากการสร้าง base type ที่ระดับ -1 ซึ่งเป็น type ช่วยใต้ type ทั้งหมดของโมเดล
  • สมาชิกของ type นี้เรียกว่า atoms แต่ไม่ได้เป็น atom ในความหมายของ ZFU หรือ NFU
  • มี atom จำนวน μ ตัว และถูกแบ่งเป็น litters ที่มีขนาด κ

• t-set และ allowable permutations

  • ในแต่ละ type level α จะสร้าง collection ที่จะเป็นสมาชิกของโมเดล TTT เรียกว่า t-set
  • พร้อมกันนั้นจะสร้าง group ของ permutation ที่กระทำกับ t-set เรียกว่า allowable permutations
  • ความสัมพันธ์การเป็นสมาชิกถูกคงไว้ภายใต้การกระทำของ allowable permutations
  • t-set แต่ละตัวถูกกำหนดให้มี support สำหรับการกระทำของ allowable permutations
  • support คือเซตขนาดเล็กของวัตถุที่เรียกว่า addresses
  • หาก allowable permutation ตัวใดตรึงสมาชิกทุกตัวของ support ไว้ t-set นั้นก็จะถูกตรึงไว้ด้วย

• ปรับ extensionality ด้วย preferred extension

  • t-set ในแต่ละ level α มี preferred extension ของ type บางตัว β < α
  • สามารถกู้คืนได้จากสมาชิกของ t-set ว่า extension ใดเป็นที่ต้องการ และ extension ของ type ที่ต่ำกว่าอื่น ๆ ได้มาจาก β-extension นั้น
  • โครงสร้างนี้ใช้เพื่อทำให้สอดคล้องกับสัจพจน์ extensionality ของ TTT

• การควบคุมขนาดของ type

  • type α แต่ละตัวจะสร้างได้ก็ต่อเมื่อมีสมมติฐาน เช่น type ทุกตัว β < α มีขนาดเท่ากับ μ พอดี
  • พิสูจน์ได้ง่ายว่า collection ของ t-set ที่ level α มีขนาดอย่างน้อย μ ดังนั้นต้องแสดงว่ามีมากที่สุด μ ตัว
  • เพื่อสิ่งนี้ จะแสดงว่าไม่มีการบรรยาย tangles ที่แตกต่างกันโดยพื้นฐานจำนวนมากนักภายใต้การกระทำของ allowable permutations
  • ขั้นตอนนี้ต้องใช้ lemma เชิงเทคนิคคือ freedom of action theorem ซึ่งช่วยให้สร้าง allowable permutations ได้
  • ผลลัพธ์หลักของส่วนนี้อยู่ที่ ConNF.mk_tSet

• การปิดงานด้วย induction และการตรวจสอบสัจพจน์

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

[GN⁺]

ความคิดเห็นบน Hacker News

• ผมมองว่าความเสี่ยงที่พิสูจน์ใน Lean จะผิดนั้นน้อยมาก
  อย่างไรก็ตาม แม้จะไม่เกี่ยวกับบั๊กของ Lean ก็ยังมีความเสี่ยงที่รู้กันดีทั้งในการตรวจสอบซอฟต์แวร์และในคณิตศาสตร์: ต้อง อ่านข้อสรุปให้ถูกต้องและตรวจสอบว่าสิ่งที่พิสูจน์ได้คือประพจน์ที่ต้องการจริง ๆ หรือไม่
  ผมอ่านข้อสรุปสุดท้ายของ Wilshaw อย่างละเอียดแล้ว และตัดสินว่าเขาพิสูจน์สิ่งที่ควรต้องพิสูจน์จริง ๆ

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

  • ปัญหาที่ผมพูดถึงเชื่อมโยงกับความกังวลเรื่องไลบรารี: หากใช้แนวคิดที่ถูกนิยามไว้บางอย่าง ก็ต้องมั่นใจว่านิยามนั้นถูกต้อง กล่าวคือ สิ่งที่พิสูจน์ได้นั้นเป็นสิ่งที่ต้องการจริง ๆ
    การ formalize ของ Wilshaw แม้จะใช้ไลบรารี แต่ไม่เปราะบางต่อข้อโต้แย้งนี้ สิ่งที่พิสูจน์ได้คือแนวคิดที่นิยามไว้บางอย่างสอดคล้องกับชุดเฉพาะของสูตรในตรรกะอันดับหนึ่ง และหากมีเพรดิเคตที่สอดคล้องกับสูตรเหล่านั้น NF ก็ consistent

  • ความเสี่ยงอีกอย่างคือบั๊กใน Lean เอง เรื่องนี้ไม่ใช่สิ่งที่ไม่เคยเกิดขึ้นมาก่อนใน theorem prover 1
    อาจเป็นเรื่องยากที่จะบังเอิญไปเจอเข้า แต่ความร่วมมือขนาดใหญ่ที่ให้คนทั่วไปช่วยเติมขั้นตอนต่าง ๆ อย่างใน 3 กำลังเติบโตขึ้นเรื่อย ๆ สถานการณ์ที่มีใครบางคนใช้บั๊กที่ค้นพบมาเติมขั้นตอนหนึ่งเพื่อก่อกวน อาจกลายเป็นเรื่องที่น่ากังวลได้

  • จากมุมมองของ foundational theory สิ่งสำคัญอีกอย่างคือพิสูจน์นี้เป็นพิสูจน์เกี่ยวกับ equiconsistency ระหว่าง NF กับ Lean kernel ตัว Lean kernel เองนั้นมนุษย์เป็นผู้ตรวจทาน
    theorem prover แบบกลไกทำหน้าที่รักษาระดับความถูกต้องที่ถูกป้อนเข้ามาผ่านมนุษย์หรือระบบภายนอกอื่น ๆ

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

  • นึกถึง Liquid Tensor Experiment ด้วย

    https://www.nature.com/articles/d41586-021-01627-2

    https://leanprover-community.github.io/blog/posts/lte-final/

  • เป็นสถานการณ์คล้ายกับ Kepler conjecture (https://en.m.wikipedia.org/wiki/Kepler_conjecture)
    พิสูจน์เป็นที่รู้จักอยู่แล้ว แต่ก่อนจะถูก formalize ก็ยังไม่มั่นใจว่าถูกต้องหรือไม่

  • ถัดไปน่าจะเป็นคิวของ abc conjecture
    มีการอ้างว่าพิสูจน์ได้ในปี 2012 และมีบทความยาวกว่า 400 หน้าออนไลน์อยู่ แต่ดูเหมือนไม่มีคนจำนวนมากที่ยอมรับพิสูจน์นั้น

• ช่วยอธิบายคร่าว ๆ ได้ไหมว่า formalization ของทฤษฎีเซต “New Foundations” มีอะไรพิเศษหรือใหม่เมื่อเทียบกับ formalization แบบอื่น ๆ?
  หรือถ้ามีลิงก์คำอธิบายที่นักศึกษาปริญญาตรีคณิตศาสตร์หรือผู้เชี่ยวชาญด้านวิศวกรรมอ่านได้ก็ได้

  • ผมเพิ่งแก้บทความ Wikipedia ไป ตอนนี้น่าจะอ่านง่ายขึ้นแล้ว: https://en.wikipedia.org/wiki/New_Foundations
    แก่นสำคัญคือการมีอยู่ของ universal set ในงานที่ผมใช้ คือระบบชนิดข้อมูลของภาษาโปรแกรม universal set แบบนี้มีประโยชน์มาก
    ทางเลี่ยงหลายแบบในระบบเดิม เช่น cumulative universes หรือ type-in-type ยังไม่น่าพอใจ แทนที่จะทำแบบนั้น เราสามารถตรวจเพียงว่า type signature ถูก stratify หรือไม่ แล้วลืมไปได้ว่าชนิดข้อมูลมีระดับเป็นตัวเลขอยู่
  • สิ่งที่ผมชอบมากในเชิงสุนทรียะของ NF คือวิธีที่มันปรับ axiom ของการเลือกสับเซต เพื่อไม่ให้ “เซตของเซตทั้งหมด” ก่อให้เกิด Russell’s paradox
    โดยพื้นฐานแล้ว มันกำหนดให้เพรดิเคตที่ใช้เลือกสับเซตต้องเป็นไปตามระบบชนิดข้อมูลที่เบามาก “x ไม่ใช่สมาชิกของตัวมันเอง” ไม่ใช่คำถามที่มีชนิดข้อมูลถูกต้องในระบบชนิดข้อมูลที่สมเหตุสมผล และโดยเฉพาะอย่างยิ่งก็ไม่เป็นไปตามข้อกำหนด “stratifiability” ของ NF ดังนั้นจึงไม่สามารถสร้างเซตแบบ Russell’s paradox ซึ่งเป็นเซตของเซตทั้งหมดที่ไม่ประกอบด้วยตัวเองได้
  • จุดที่ “ดี” อย่างหนึ่งของ NF คือมี axiom/axiom schema เพียงสองข้อ: 1) เซตที่มีสมาชิกเหมือนกันย่อมเท่ากัน, 2) สำหรับ สมบัติที่สามารถ stratify ได้ ใด ๆ จะมีเซตของทุกสิ่งที่มีสมบัตินั้นสอดคล้องอยู่
    นิยามของ “สามารถ stratify ได้” ก็ไม่ได้ซับซ้อนนัก ในทางกลับกัน ZF มี axiom/axiom schema ถึงแปดข้อที่ดูค่อนข้างเหมือนการแก้ปัญหาเฉพาะหน้า

• ผมอยากรู้ว่าความแตกต่างพื้นฐานระหว่าง Coq กับ Lean คืออะไร และทั้งสองทำงานบนตรรกะประเภทเดียวกันหรือไม่ เลยไปเจอบทความนี้ 1
  ผมแทบไม่เข้าใจการอภิปรายในนั้น และก็ไม่ได้ใช้ทั้งสองจริง ๆ หากมีอะไรเพิ่มเติมในประเด็นนี้ หรือมีการเปรียบเทียบกับ proof assistant ตัวอื่น ๆ ก็อยากฟัง

  1 https://proofassistants.stackexchange.com/questions/153/what...

  • มีความแตกต่างกัน และการอภิปรายนี้ก็น่าอ่าน 1

    1 https://github.com/coq/coq/issues/10871

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

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

  • อาจมีบั๊กได้ก็จริง แต่เท่าที่ผมเข้าใจ สิ่งเดียวที่ต้องเชื่อถือคือ เคอร์เนล
    ถ้า “สแต็กไลบรารีจำนวนมากที่เขียนโดยมนุษย์คนอื่น ๆ” หมายถึง mathlib ผมคิดว่าคำพูดนั้นไม่ค่อยถูก เพราะโค้ดของ mathlib สุดท้ายก็ถูกคอมไพล์เป็นโค้ดที่เคอร์เนลประมวลผลอยู่ดี
    ร่างบทความบนเว็บไซต์ 0 ก็ย้ำจุดนี้เช่นกัน: Lean เป็นโปรเจกต์ขนาดใหญ่ แต่เพื่อรับประกันว่าพิสูจน์ที่ถูกยอมรับนั้นถูกต้อง เราต้องเชื่อถือแค่เคอร์เนลเท่านั้น แม้ tactic จะส่งออกเทอมพิสูจน์ที่ผิด เคอร์เนลก็ยังมีโอกาสจับข้อผิดพลาดนั้นก่อนจะยอมรับพิสูจน์

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

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

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

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

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

    1. พิสูจน์ได้ว่า NF ขัดแย้งกันเอง ถ้าอย่างนั้น ZFC ก็ขัดแย้งกันเองด้วย ดวงดาวบนท้องฟ้ายามค่ำคืนจะเริ่มดับไปทีละดวง ;)

    2. พิสูจน์ได้ว่า ZFC ขัดแย้งกันเอง ถ้าอย่างนั้น NF ก็ยังอาจสอดคล้องกันอยู่ ต้องหวังพึ่งโชคแล้ว

    แน่นอนว่าผมอาจพลาดข้อดีเชิง “คุณภาพชีวิต” ที่ใช้งานได้จริงกว่าของ NF เช่น การพูดถึงคลาสที่แท้จริงได้ หรือการหลีกเลี่ยงปฏิทรรศน์ของ Russell ด้วยสูตรแบบ stratified

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

• ผมชอบเรื่องนี้มากจริง ๆ
  สุดท้ายมันจะนำไปสู่ พิสูจน์แบบร่วมมือกัน และ “การแก้บั๊ก” จนคณิตศาสตร์กลายเป็นกระบวนการคล้ายโค้ดบน GitHub ไหมนะ

  • มันกำลังเป็นแบบนั้นอยู่แล้ว ดู Lean blueprint ได้: https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
  • แนวคิดเรื่องพิสูจน์แบบร่วมมือกันมีมานานพอสมควรแล้ว อย่างน้อยก็ 10 ปี: https://arxiv.org/abs/1404.6186

• ถ้ามีเวลาว่างพอจะติดตามโปรเจกต์ mathlib ก็คงดี มันเจ๋งมากจริง ๆ
  มีวิธีเข้าร่วมแบบหลวม ๆ มาก ๆ บ้างไหม?

  • เริ่มจาก Natural numbers game ได้

    https://adam.math.hhu.de/#/g/leanprover-community/NNG4

• ไม่ได้อยู่ในสายนี้โดยตรง แต่มี ทฤษฎีบทของ Gödel ที่บอกว่าระบบทุกระบบที่แข็งแรงพอไม่สามารถแสดงความสอดคล้องของตัวเองได้ไม่ใช่หรือ?

  • สิ่งที่นึกถึงน่าจะเป็นทฤษฎีบทความไม่สมบูรณ์ของ Gödel: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
    แต่แม้ระบบ X จะพิสูจน์ความสอดคล้องของตัวเองไม่ได้ ระบบ Y ที่แข็งแรงกว่าสามารถพิสูจน์ความสอดคล้องของ X ได้ และระบบอื่นที่แข็งแรงกว่านั้นก็อาจพิสูจน์ความสอดคล้องของ Y ได้เช่นกัน จึงเกิดเป็นห่วงโซ่ที่แต่ละระบบพิสูจน์ความสอดคล้องของระบบที่อ่อนแอกว่า
    สิ่งนี้ไม่ได้พิสูจน์ว่าระบบนั้นสอดคล้องอย่างสัมบูรณ์ เพราะถ้า Y มีความขัดแย้ง ก็สามารถพิสูจน์ได้ทั้งว่า X สอดคล้อง และว่า X มีความขัดแย้ง ถึงอย่างนั้นก็ยังมีคุณค่าอยู่ดี เพราะหนึ่งในเหตุผลที่เราใช้ Y ก็คือเราไม่รู้จักความขัดแย้งภายในมัน ระบบเชิงรูปนัยมักอาจมีความขัดแย้งอย่างแยบยลได้ ดังนั้น “สอดคล้องภายใต้สมมติฐานว่าอีกระบบหนึ่งสอดคล้อง” จึงดีกว่า “ไม่มีหลักฐานความสอดคล้องเลย” มาก
  • ในที่นี้ ระบบนั้นไม่ได้พิสูจน์ความสอดคล้องของตัวเอง แต่พิสูจน์ความสอดคล้องใน อีกระบบหนึ่งที่แข็งแรงกว่า
  • จุดที่น่าสนใจคือ ต่อให้ระบบที่แข็งแรงสามารถพิสูจน์ความสอดคล้องของตัวเองได้ เพียงเท่านั้นก็ยังทำให้เรารู้อะไรไม่ได้
    ระบบที่มีความขัดแย้งก็สามารถพิสูจน์ความสอดคล้องของตัวเองได้เช่นกัน ดังนั้นแม้ระบบใดระบบหนึ่งจะมีหลักฐานพิสูจน์ว่าตัวมันเองสอดคล้อง เราก็ยังไม่อาจรู้ได้อยู่ดีว่ามันสอดคล้องจริงหรือไม่
  • หลักฐานพิสูจน์นี้ควรเข้าใจว่า “ถ้า Lean 4 สอดคล้อง New Foundations ก็สอดคล้องด้วย” ซึ่งไม่ขัดกับทฤษฎีบทความไม่สมบูรณ์ของ Gödel
  • ระบบในที่นี้ดูเหมือนไม่ได้พยายามพิสูจน์สมมติฐานฐานรากของตัวเอง แต่สร้างต่อยอดบนชุดสมมติฐานที่มีอยู่เดิม ทฤษฎีบทที่นึกถึงน่าจะไม่ได้นำมาใช้ได้

• การอภิปรายใน Reddit ที่หนึ่งในผู้สร้างเข้าร่วมก็น่าอ่านเช่นกัน 0

  https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...